1  /-
  2  Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Sébastien Gouëzel
  5  -/
  6  
  7  import topology.metric_space.isometry topology.instances.ennreal
src         └────────────────────────────┘ └────────────────────────┘
  8         topology.metric_space.lipschitz
src         └─────────────────────────────┘
  9  
 10  /-!
 11  # Hausdorff distance
 12  
 13  The Hausdorff distance on subsets of a metric (or emetric) space.
 14  
 15  Given two subsets `s` and `t` of a metric space, their Hausdorff distance is the smallest `d`
 16  such that any point `s` is within `d` of a point in `t`, and conversely. This quantity
 17  is often infinite (think of `s` bounded and `t` unbounded), and therefore better
 18  expressed in the setting of emetric spaces.
 19  
 20  ## Main definitions
 21  
 22  This files introduces:
 23  * `inf_edist x s`, the infimum edistance of a point `x` to a set `s` in an emetric space
 24  * `Hausdorff_edist s t`, the Hausdorff edistance of two sets in an emetric space
 25  * Versions of these notions on metric spaces, called respectively `inf_dist` and
 26  `Hausdorff_dist`.
 27  -/
 28  noncomputable theory
 29  open_locale classical
 30  universes u v w
 31  
 32  open classical lattice set function topological_space filter
 33  
 34  namespace emetric
 35  
 36  section inf_edist
 37  open_locale ennreal
 38  variables {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {x y : α} {s t : set α} {Φ : α → β}
id                                        └───────────┘     └───────────┘                     └─┘
src                                       └───────────┘     └───────────┘                     └─┘
typ                                       └───────────┘     └───────────┘                     └─┘
doc                                       └───────────┘     └───────────┘
 39  
 40  /-- The minimal edistance of a point to a set -/
 41  def inf_edist (x : α) (s : set α) : ennreal := Inf ((edist x) '' s)
id                             └─┘     └─────┘    └─┘   └───┘   └┘ 
src                             └─┘      └─────┘    └─┘   └───┘    └┘
typ                            └─┘     └─────┘    └─┘   └───┘   └┘ 
doc                                      └─────┘    └─┘
 42  
 43  @[simp] lemma inf_edist_empty : inf_edist x ∅ = ∞ :=
id                                   └───────┘    
src                                  └───────┘     
typ                                  └───────┘    
doc    └──┘                          └───────┘       
 44  by unfold inf_edist; simp
src     └──────────────┘  └────
typ     └──────────────┘  └────
doc     └──────────────┘  └────
txt     └──────────────┘  └────
par     └──────────────┘  └────
pid           └────────┘      
st     └───────────────────────
 45  
src  
typ  
doc  
txt  
par  
pid  
st   
 46  /-- The edist to a union is the minimum of the edists -/
 47  @[simp] lemma inf_edist_union : inf_edist x (s ∪ t) = inf_edist x s ⊓ inf_edist x t :=
id                                   └───────┘        └───────┘    └───────┘  
src                                  └───────┘           └───────┘      └───────┘
typ                                  └───────┘        └───────┘    └───────┘  
doc    └──┘                          └───────┘             └───────┘       └───────┘
 48  by simp [inf_edist, image_union, Inf_union]
src     └────┘         └┘           └┘         └─
typ     └────┘         └┘           └┘         └─
doc     └────┘         └┘           └┘         └─
txt     └────┘         └┘           └┘         └─
par     └────┘         └┘           └┘         └─
pid                  └┘           └┘         
 49  
src  
typ  
doc  
txt  
par  
pid  
 50  /-- The edist to a singleton is the edistance to the single point of this singleton -/
 51  @[simp] lemma inf_edist_singleton : inf_edist x {y} = edist x y :=
doc    └──┘
 52  by simp [inf_edist]
src     └────┘         └─
typ     └────┘         └─
doc     └────┘         └─
txt     └────┘         └─
par     └────┘         └─
pid                  
 53  
src  
typ  
doc  
txt  
par  
pid  
 54  /-- The edist to a set is bounded above by the edist to any of its points -/
 55  lemma inf_edist_le_edist_of_mem (h : y ∈ s) : inf_edist x s ≤ edist x y :=
id                                              └───────┘    └───┘  
src                                               └───────┘      └───┘
typ                                             └───────┘    └───┘  
doc                                                └───────┘
 56  Inf_le ((mem_image _ _ _).2 ⟨y, h, by refl⟩)
id   └────┘   └───────┘            
src  └────┘   └───────┘                   └──┘
typ  └────┘   └───────┘                 └──┘
doc                                        └──┘
txt                                        └──┘
par                                        └──┘
st                                        └───┘
 57  
 58  /-- If a point `x` belongs to `s`, then its edist to `s` vanishes -/
 59  lemma inf_edist_zero_of_mem (h : x ∈ s) : inf_edist x s = 0 :=
id                                          └───────┘   
src                                           └───────┘     
typ                                         └───────┘   
doc                                            └───────┘
 60  le_zero_iff_eq.1 $ @edist_self _ _ x ▸ inf_edist_le_edist_of_mem h
id   └────────────┘     └────────┘       └───────────────────────┘ 
src  └────────────┘     └────────┘        └───────────────────────┘
typ  └────────────┘     └────────┘       └───────────────────────┘ 
doc                                         └───────────────────────┘
 61  
 62  /-- The edist is monotonous with respect to inclusion -/
 63  lemma inf_edist_le_inf_edist_of_subset (h : s ⊆ t) : inf_edist x t ≤ inf_edist x s :=
id                                                     └───────┘    └───────┘  
src                                                      └───────┘      └───────┘
typ                                                    └───────┘    └───────┘  
doc                                                       └───────┘       └───────┘
 64  Inf_le_Inf (image_subset _ h)
id   └────────┘  └──────────┘   
src  └────────┘  └──────────┘
typ  └────────┘  └──────────┘   
 65  
 66  /-- If the edist to a set is `< r`, there exists a point in the set at edistance `< r` -/
 67  lemma exists_edist_lt_of_inf_edist_lt {r : ennreal} (h : inf_edist x s < r) :
id                                              └─────┘       └───────┘    
src                                             └─────┘       └───────┘     
typ                                             └─────┘       └───────┘    
doc                                             └─────┘       └───────┘
 68    ∃y∈s, edist x y < r :=
id       └───┘    
src        └───┘     
typ      └───┘    
 69  let ⟨t, ⟨ht, tr⟩⟩ :=  Inf_lt_iff.1 h in
id   └─┘      └┘           └────────┘  
src                        └────────┘
typ  └─┘      └┘           └────────┘  
 70  let ⟨y, ⟨ys, hy⟩⟩ := (mem_image _ _ _).1 ht in
id   └─┘     └┘           └───────┘       
src                        └───────┘       
typ  └─┘     └┘           └───────┘       
 71  ⟨y, ys, by rwa ← hy at tr⟩
id                    └┘
src             └────┘  └────┘
typ             └────┘└┘└────┘
doc             └────┘  └────┘
txt             └────┘  └────┘
par             └────┘  └────┘
pid                └─┘  └────┘
st             └─────────────┘
 72  
 73  /-- The edist of `x` to `s` is bounded by the sum of the edist of `y` to `s` and
 74  the edist from `x` to `y` -/
 75  lemma inf_edist_le_inf_edist_add_edist : inf_edist x s ≤ inf_edist y s + edist x y :=
id                                            └───────┘    └───────┘    └───┘  
src                                           └───────┘      └───────┘      └───┘
typ                                           └───────┘    └───────┘    └───┘  
doc                                           └───────┘       └───────┘
 76  begin
st   └─────
 77    have : ∀z ∈ s, Inf (edist x '' s) ≤ edist y z + edist x y := λz hz, calc
id                    └─┘          └┘               └───┘  
src    └─────┘ └──┘  └─┘       └┘ └┘       └───┘  └──┘ └────┘    
typ    └─────┘ └──┘  └─┘       └┘└┘       └───┘└──┘ └────┘    
doc    └─────┘ └──┘  └─┘          └┘                └──┘ └────┘    
txt    └─────┘ └──┘               └┘                └──┘ └────┘    
par    └─────┘ └──┘               └┘                └──┘ └────┘    
pid    └───┘└┘ └──┘               └┘                └──┘ └────┘    
st   ───────────────────────────────────────────────────────────────────────────
 78      Inf (edist x '' s) ≤ edist x z :
id       └─┘                 └───┘ 
src  ───┘└─┘          └┘ └───┘  └──
typ  ───┘└─┘         └┘ └───┘ └──
doc  ───┘└─┘          └┘        └──
txt  ───┘             └┘        └──
par  ───┘             └┘        └──
pid  ───┘             └┘        └──
st   ─────────────────────────────────────
 79        Inf_le ((mem_image _ _ _).2 ⟨z, hz, by refl⟩)
id         └────┘   └───────┘
src  ─────┘└────┘  └───────┘└────────┘  └┘  └┘  └──┘└──
typ  ─────┘└────┘  └───────┘└────────┘  └┘  └┘  └──┘└──
doc  ─────┘                 └────────┘  └┘  └┘  └──┘└──
txt  ─────┘                 └────────┘  └┘  └┘  └──┘└──
par  ─────┘                 └────────┘  └┘  └┘  └──┘└──
pid  ─────┘                 └────────┘  └┘  └┘  └───────
st   ───────────────────────────────────────────┘└───┘└──
 80      ... ≤ edist x y + edist y z : edist_triangle _ _ _
id                                     └────────────┘
src  ───────┘                └─┘└────────────┘└──────
typ  ───────┘                └─┘└────────────┘└──────
doc  ───────┘                └─┘              └──────
txt  ───────┘                └─┘              └──────
par  ───────┘                └─┘              └──────
pid  ───────┘                └─┘              └──────
st   ───────────────────────────────────────────────────────
 81      ... = edist y z + edist x y : add_comm _ _,
id                                    └──────┘
src  ───────┘                └─┘└──────┘└──┘
typ  ───────┘               └─┘└──────┘└──┘
doc  ───────┘                └─┘        └──┘
txt  ───────┘                └─┘        └──┘
par  ───────┘                └─┘        └──┘
pid  ───────┘                └─┘        └──┘
st   ─────────────────────────────────────────────┘└─
 82    have : (λz, z + edist x y) (Inf (edist y '' s)) = Inf ((λz, z + edist x y) '' (edist y '' s)),
id                                                      └─┘                         └───┘     
src    └─────┘  └─┘         └┘              └─┘└─┘   └─┘         └┘   └───┘    └┘
typ    └─────┘  └─┘         └┘              └─┘└─┘   └─┘        └┘   └───┘  └┘
doc    └─────┘  └─┘         └┘              └─┘ └─┘   └─┘         └┘            └┘
txt    └─────┘  └─┘         └┘              └─┘       └─┘         └┘            └┘
par    └─────┘  └─┘         └┘              └─┘       └─┘         └┘            └┘
pid    └───┘└┘  └─┘         └┘              └─┘       └─┘         └┘            └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
 83    { refine Inf_of_continuous _ _ (by simp),
id              └───────────────┘
src      └─────┘└───────────────┘└───┘   └──┘
typ      └─────┘└───────────────┘└───┘   └──┘
doc      └─────┘└───────────────┘└───┘   └──┘
txt      └─────┘                 └───┘   └──┘
par      └─────┘                 └───┘   └──┘
pid                             └───┘   └────┘
st   ───┘└──────────────────────────────┘└───┘└─
 84      { exact continuous_id.add continuous_const },
id               └───────────────┘ └──────────────┘
src        └────┘└───────────────┘└──────────────┘
typ        └────┘└───────────────┘└──────────────┘
doc        └────┘                                 
txt        └────┘                                 
par        └────┘                                 
pid                                              
st   ─────┘└───────────────────────────────────────┘└┘
 85      { assume a b h, simp, apply add_le_add_right' h }},
id                                   └───────────────┘ 
src        └──────────┘  └──┘  └────┘└───────────────┘ 
typ        └──────────┘  └──┘  └────┘└───────────────┘
doc        └──────────┘  └──┘  └────┘                  
txt        └──────────┘  └──┘  └────┘                  
par        └──────────┘  └──┘  └────┘                  
pid        └──────────┘                               
st   ─────────────────┘└────┘└──────────────────────────┘└─┘
 86    simp only [inf_edist] at this,
id                └───────┘
src    └─────────┘└───────┘└───────┘
typ    └─────────┘└───────┘└───────┘
doc    └─────────┘└───────┘└───────┘
txt    └─────────┘         └───────┘
par    └─────────┘         └───────┘
pid        └──┘└┘         └─────┘
st   ──────────────────────────────┘└─
 87    rw [inf_edist, inf_edist, this, ← image_comp],
id         └───────┘  └───────┘  └──┘    └────────┘
src    └──┘└───────┘└┘└───────┘└┘    └──┘└────────┘
typ    └──┘└───────┘└┘└───────┘└┘└──┘└──┘└────────┘
doc    └──┘└───────┘└┘└───────┘└┘    └──┘          
txt    └──┘         └┘         └┘    └──┘          
par    └──┘         └┘         └┘    └──┘          
pid      └┘         └┘         └┘    └──┘          
st   ──────────────┘└─────────┘└────┘└────────────┘└──
 88    simpa only [and_imp, function.comp_app, lattice.le_Inf_iff, exists_imp_distrib, ball_image_iff]
id                 └─────┘  └───────────────┘  └────────────────┘  └────────────────┘  └────────────┘
src    └──────────┘└─────┘└┘└───────────────┘└┘└────────────────┘└┘└────────────────┘└┘└────────────┘└┘
typ    └──────────┘└─────┘└┘└───────────────┘└┘└────────────────┘└┘└────────────────┘└┘└────────────┘└┘
doc    └──────────┘       └┘                 └┘                  └┘                  └┘              └┘
txt    └──────────┘       └┘                 └┘                  └┘                  └┘              └┘
par    └──────────┘       └┘                 └┘                  └┘                  └┘              └┘
pid         └──┘└┘       └┘                 └┘                  └┘                  └┘              
st   ─────────────────────────────────────────────────────────────────────────────────────────────────┘
 89  end
st   └─┘
 90  
 91  /-- The edist to a set depends continuously on the point -/
 92  lemma continuous_inf_edist : continuous (λx, inf_edist x s) :=
id                                └────────┘     └───────┘  
src                               └────────┘      └───────┘
typ                               └────────┘     └───────┘  
doc                               └────────┘      └───────┘
 93  continuous_of_le_add_edist 1 (by simp) $
id   └────────────────────────┘
src  └────────────────────────┘       └──┘
typ  └────────────────────────┘       └──┘
doc                                   └──┘
txt                                   └──┘
par                                   └──┘
st                                   └───┘
 94    by simp only [one_mul, inf_edist_le_inf_edist_add_edist, forall_2_true_iff]
id                   └─────┘  └──────────────────────────────┘  └───────────────┘
src       └─────────┘└─────┘└┘└──────────────────────────────┘└┘└───────────────┘└─
typ       └─────────┘└─────┘└┘└──────────────────────────────┘└┘└───────────────┘└─
doc       └─────────┘       └┘└──────────────────────────────┘└┘                 └─
txt       └─────────┘       └┘                                └┘                 └─
par       └─────────┘       └┘                                └┘                 └─
pid           └──┘└┘       └┘                                └┘                 
st       └─────────────────────────────────────────────────────────────────────────
 95  
src  
typ  
doc  
txt  
par  
pid  
st   
 96  /-- The edist to a set and to its closure coincide -/
 97  lemma inf_edist_closure : inf_edist x (closure s) = inf_edist x s :=
id                             └───────┘   └─────┘    └───────┘  
src                            └───────┘    └─────┘     └───────┘
typ                            └───────┘   └─────┘    └───────┘  
doc                            └───────┘    └─────┘      └───────┘
 98  begin
st   └─────
 99    refine le_antisymm (inf_edist_le_inf_edist_of_subset subset_closure) _,
id            └─────────┘  └──────────────────────────────┘ └────────────┘
src    └─────┘└─────────┘ └──────────────────────────────┘└────────────┘└─┘
typ    └─────┘└─────────┘ └──────────────────────────────┘└────────────┘└─┘
doc    └─────┘            └──────────────────────────────┘              └─┘
txt    └─────┘                                                          └─┘
par    └─────┘                                                          └─┘
pid                                                                    └─┘
st   ───────────────────────────────────────────────────────────────────────┘└─
100    refine ennreal.le_of_forall_epsilon_le (λε εpos h, _),
id            └─────────────────────────────┘
src    └─────┘└─────────────────────────────┘  └──────────┘
typ    └─────┘└─────────────────────────────┘  └──────────┘
doc    └─────┘                                 └──────────┘
txt    └─────┘                                 └──────────┘
par    └─────┘                                 └──────────┘
pid                                           └──────────┘
st   ──────────────────────────────────────────────────────┘└─
101    have εpos' : (0 : ennreal) < ε := by simpa,
id                       └─────┘   
src    └───────────┘ └──┘└─────┘└┘ └──┘  └───┘
typ    └───────────┘ └──┘└─────┘└┘└──┘  └───┘
doc    └───────────┘ └──┘└─────┘└┘  └──┘  └───┘
txt    └───────────┘ └──┘       └┘  └──┘  └───┘
par    └───────────┘ └──┘       └┘  └──┘  └───┘
pid    └────────┘└─┘ └──┘       └┘  └──┘  └────┘
st   ─────────────────────────────────────┘└────┘└─
102    have : inf_edist x (closure s) < inf_edist x (closure s) + ε/2 :=
id                                      └───────┘   └─────┘    
src    └─────┘                   └┘ └───────┘  └─────┘ └┘ └────
typ    └─────┘                   └┘ └───────┘ └─────┘└┘└────
doc    └─────┘                   └┘ └───────┘  └─────┘ └┘   └────
txt    └─────┘                   └┘                    └┘   └────
par    └─────┘                   └┘                    └┘   └────
pid    └───┘└┘                   └┘                    └┘   └────
st   ────────────────────────────────────────────────────────────────────
103      ennreal.lt_add_right h (ennreal.half_pos εpos'),
id       └──────────────────┘   └──────────────┘ └───┘
src  ───┘└──────────────────┘  └──────────────┘     
typ  ───┘└──────────────────┘ └──────────────┘└───┘
doc  ───┘                                           
txt  ───┘                                           
par  ───┘                                           
pid  ───┘                                           
st   ──────────────────────────────────────────────────┘└─
104    rcases exists_edist_lt_of_inf_edist_lt this with ⟨y, ycs, hy⟩,
id            └─────────────────────────────┘ └──┘
src    └─────┘└─────────────────────────────┘    └────────────────┘
typ    └─────┘└─────────────────────────────┘└──┘└────────────────┘
doc    └─────┘└─────────────────────────────┘    └────────────────┘
txt    └─────┘                                   └────────────────┘
par    └─────┘                                   └────────────────┘
pid                                             └────────────────┘
st   ──────────────────────────────────────────────────────────────┘└─
105    -- y : α,  ycs : y ∈ closure s,  hy : edist x y < inf_edist x (closure s) + ↑ε / 2
st   ──────────────┘└────────────────────────────────────────────────────────────────────
106    rcases emetric.mem_closure_iff'.1 ycs (ε/2) (ennreal.half_pos εpos') with ⟨z, zs, dyz⟩,
id            └──────────────────────┘   └─┘       └──────────────┘ └───┘
src    └─────┘└──────────────────────┘└─┘      └─┘ └──────────────┘     └─────────────────┘
typ    └─────┘└──────────────────────┘└─┘└─┘  └─┘ └──────────────┘└───┘└─────────────────┘
doc    └─────┘└──────────────────────┘└─┘      └─┘                      └─────────────────┘
txt    └─────┘                        └─┘      └─┘                      └─────────────────┘
par    └─────┘                        └─┘      └─┘                      └─────────────────┘
pid                                  └─┘      └─┘                      └─────────────────┘
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
107    -- z : α,  zs : z ∈ s,  dyz : edist y z < ↑ε / 2
st   ───────────────────────────────────────────────────
108    calc inf_edist x s ≤ edist x z : inf_edist_le_edist_of_mem zs
id     └──┘                 └───┘     └───────────────────────┘ └┘
src    └──┘                 └───┘       └───────────────────────┘
typ    └──┘                 └───┘     └───────────────────────┘ └┘
doc    └──┘                             └───────────────────────┘
st   ────────────────────────────────────────────────────────────────
109          ... ≤ edist x y + edist y z : edist_triangle _ _ _
id                                        └────────────┘
src                                        └────────────┘
typ                                       └────────────┘
st   ───────────────────────────────────────────────────────────
110          ... ≤ (inf_edist x (closure s) + ε / 2) + (ε/2) : add_le_add' (le_of_lt hy) (le_of_lt dyz)
id                                                             └─────────┘           └┘   └──────┘ └─┘
src                                                            └─────────┘                └──────┘
typ                                                            └─────────┘           └┘   └──────┘ └─┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────────
111          ... = inf_edist x (closure s) + ↑ε : by simp [ennreal.add_halves]
id                 └───────┘    └─────┘                 └────────────────┘
src                └───────┘    └─────┘             └────┘└────────────────┘└┘
typ                └───────┘    └─────┘           └────┘└────────────────┘└┘
doc                └───────┘    └─────┘              └────┘                  └┘
txt                                                  └────┘                  └┘
par                                                  └────┘                  └┘
pid                                                                        
st   ──────────────────────────────────────────────┘└─────────────────────────┘
112  end
st   └─┘
113  
114  /-- A point belongs to the closure of `s` iff its infimum edistance to this set vanishes -/
115  lemma mem_closure_iff_inf_edist_zero : x ∈ closure s ↔ inf_edist x s = 0 :=
id                                            └─────┘   └───────┘   
src                                            └─────┘    └───────┘     
typ                                           └─────┘   └───────┘   
doc                                             └─────┘     └───────┘
116  ⟨λh, by rw ← inf_edist_closure; exact inf_edist_zero_of_mem h,
id               └───────────────┘        └───────────────────┘ 
src          └───┘└───────────────┘  └────┘└───────────────────┘
typ         └───┘└───────────────┘  └────┘└───────────────────┘
doc          └───┘└───────────────┘  └────┘└───────────────────┘
txt          └───┘                   └────┘                     
par          └───┘                   └────┘                     
pid            └─┘                                             
st          └────────────────────────────────────────────────────┘
117  λh, emetric.mem_closure_iff'.2 $ λε εpos, exists_edist_lt_of_inf_edist_lt (by rwa h)⟩
id      └──────────────────────┘      └──┘  └─────────────────────────────┘         
src      └──────────────────────┘             └─────────────────────────────┘     └──┘
typ     └──────────────────────┘      └──┘  └─────────────────────────────┘     └──┘
doc      └──────────────────────┘              └─────────────────────────────┘     └──┘
txt                                                                                └──┘
par                                                                                └──┘
pid                                                                                   
st                                                                                └────┘
118  
119  /-- Given a closed set `s`, a point belongs to `s` iff its infimum edistance to this set vanishes -/
120  lemma mem_iff_ind_edist_zero_of_closed (h : is_closed s) : x ∈ s ↔ inf_edist x s = 0 :=
id                                               └───────┘         └───────┘   
src                                              └───────┘            └───────┘     
typ                                              └───────┘         └───────┘   
doc                                              └───────┘              └───────┘
121  begin
st   └─────
122    convert ← mem_closure_iff_inf_edist_zero,
id               └────────────────────────────┘
src    └────────┘└────────────────────────────┘
typ    └────────┘└────────────────────────────┘
doc    └────────┘└────────────────────────────┘
txt    └────────┘
par    └────────┘
pid           └┘
st   ─────────────────────────────────────────┘└─
123    exact closure_eq_iff_is_closed.2 h
id           └──────────────────────┘   
src    └────┘└──────────────────────┘└─┘ 
typ    └────┘└──────────────────────┘└─┘
doc    └────┘                        └─┘ 
txt    └────┘                        └─┘ 
par    └────┘                        └─┘ 
pid                                 └─┘ 
st   ────────────────────────────────────┘
124  end
st   └─┘
125  
126  /-- The infimum edistance is invariant under isometries -/
127  lemma inf_edist_image (hΦ : isometry Φ) :
id                               └──────┘ 
src                              └──────┘
typ                              └──────┘ 
doc                              └──────┘
128    inf_edist (Φ x) (Φ '' t) = inf_edist x t :=
id     └───────┘       └┘    └───────┘  
src    └───────┘          └┘     └───────┘
typ    └───────┘       └┘    └───────┘  
doc    └───────┘                  └───────┘
129  begin
st   └─────
130    simp only [inf_edist],
id                └───────┘
src    └─────────┘└───────┘
typ    └─────────┘└───────┘
doc    └─────────┘└───────┘
txt    └─────────┘         
par    └─────────┘         
pid        └──┘└┘         
st   ──────────────────────┘└─
131    apply congr_arg,
id           └───────┘
src    └────┘└───────┘
typ    └────┘└───────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────────────┘└─
132    ext b, split,
src    └───┘  └───┘
typ    └───┘  └───┘
doc    └───┘  └───┘
txt    └───┘  └───┘
par    └───┘  └───┘
pid       └┘
st   ──────┘└─────┘└─
133    { assume hb,
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
pid      └───────┘
st   ───┘└───────┘└─
134      rcases (mem_image _ _ _).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
id               └───────┘          └┘
src      └─────┘ └───────┘└────────┘  └──────────────────┘
typ      └─────┘ └───────┘└────────┘└┘└──────────────────┘
doc      └─────┘          └────────┘  └──────────────────┘
txt      └─────┘          └────────┘  └──────────────────┘
par      └─────┘          └────────┘  └──────────────────┘
pid                      └────────┘  └──────────────────┘
st   ────────────────────────────────────────────────────┘└─
135      rcases (mem_image _ _ _).1 hy with ⟨z, ⟨hz, hz'⟩⟩,
id               └───────┘          └┘
src      └─────┘ └───────┘└────────┘  └──────────────────┘
typ      └─────┘ └───────┘└────────┘└┘└──────────────────┘
doc      └─────┘          └────────┘  └──────────────────┘
txt      └─────┘          └────────┘  └──────────────────┘
par      └─────┘          └────────┘  └──────────────────┘
pid                      └────────┘  └──────────────────┘
st   ────────────────────────────────────────────────────┘└─
136      rw [← hy', ← hz', hΦ x z],
id             └─┘    └─┘  └┘  
src      └────┘   └──┘   └┘    
typ      └────┘└─┘└──┘└─┘└┘└┘
doc      └────┘   └──┘   └┘    
txt      └────┘   └──┘   └┘    
par      └────┘   └──┘   └┘    
pid        └──┘   └──┘   └┘    
st   ────────────┘└─────┘└──────┘└──
137      exact mem_image_of_mem _ hz },
id             └──────────────┘   └┘
src      └────┘└──────────────┘└─┘  
typ      └────┘└──────────────┘└─┘└┘
doc      └────┘                └─┘  
txt      └────┘                └─┘  
par      └────┘                └─┘  
pid                           └─┘  
st   ───────────────────────────────┘└┘
138    { assume hb,
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
pid      └───────┘
st   ────────────┘└─
139      rcases (mem_image _ _ _).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
id               └───────┘          └┘
src      └─────┘ └───────┘└────────┘  └──────────────────┘
typ      └─────┘ └───────┘└────────┘└┘└──────────────────┘
doc      └─────┘          └────────┘  └──────────────────┘
txt      └─────┘          └────────┘  └──────────────────┘
par      └─────┘          └────────┘  └──────────────────┘
pid                      └────────┘  └──────────────────┘
st   ────────────────────────────────────────────────────┘└─
140      rw [← hy', ← hΦ x y],
id             └─┘    └┘  
src      └────┘   └──┘    
typ      └────┘└─┘└──┘└┘
doc      └────┘   └──┘    
txt      └────┘   └──┘    
par      └────┘   └──┘    
pid        └──┘   └──┘    
st   ────────────┘└────────┘└──
141      exact mem_image_of_mem _ (mem_image_of_mem _ hy) }
id                                 └──────────────┘   └┘
src      └────┘                └─┘ └──────────────┘└─┘  └┘
typ      └────┘                └─┘ └──────────────┘└─┘└┘└┘
doc      └────┘                └─┘                 └─┘  └┘
txt      └────┘                └─┘                 └─┘  └┘
par      └────┘                └─┘                 └─┘  └┘
pid                           └─┘                 └─┘  
st   ────────────────────────────────────────────────────┘└─
142  end
st   ──┘
143  
144  end inf_edist --section
145  
146  /-- The Hausdorff edistance between two sets is the smallest `r` such that each set
147  is contained in the `r`-neighborhood of the other one -/
148  def Hausdorff_edist {α : Type u} [emetric_space α] (s t : set α) : ennreal :=
id                                     └───────────┘          └─┘     └─────┘
src                                    └───────────┘           └─┘      └─────┘
typ                                    └───────────┘          └─┘     └─────┘
doc                                    └───────────┘                    └─────┘
149    Sup ((λx, inf_edist x t) '' s) ⊔ Sup ((λx, inf_edist x s) '' t)
id     └─┘      └───────┘    └┘    └─┘      └───────┘    └┘ 
src    └─┘       └───────┘      └┘     └─┘       └───────┘      └┘
typ    └─┘      └───────┘    └┘    └─┘      └───────┘    └┘ 
doc    └─┘       └───────┘              └─┘       └───────┘
150  
151  lemma Hausdorff_edist_def {α : Type u} [emetric_space α] (s t : set α) :
id                                           └───────────┘          └─┘ 
src                                          └───────────┘           └─┘
typ                                          └───────────┘          └─┘ 
doc                                          └───────────┘
152    Hausdorff_edist s t = Sup ((λx, inf_edist x t) '' s) ⊔ Sup ((λx, inf_edist x s) '' t) := rfl
id     └─────────────┘    └─┘      └───────┘    └┘    └─┘      └───────┘    └┘      └─┘
src    └─────────────┘      └─┘       └───────┘      └┘     └─┘       └───────┘      └┘       └─┘
typ    └─────────────┘    └─┘      └───────┘    └┘    └─┘      └───────┘    └┘      └─┘
doc    └─────────────┘       └─┘       └───────┘              └─┘       └───────┘
153  
154  attribute [irreducible] Hausdorff_edist
id                           └─────────────┘
src             └─────────┘  └─────────────┘
typ                          └─────────────┘
doc             └─────────┘  └─────────────┘
155  
156  section Hausdorff_edist
157  open_locale ennreal
158  variables {α : Type u} {β : Type v} [emetric_space α] [emetric_space β]
id                                       └───────────┘     └───────────┘
src                                       └───────────┘     └───────────┘
typ                                      └───────────┘     └───────────┘
doc                                       └───────────┘     └───────────┘
159            {x y : α} {s t u : set α} {Φ : α → β}
id                                └─┘
src                               └─┘
typ                               └─┘
160  
161  /-- The Hausdorff edistance of a set to itself vanishes -/
162  @[simp] lemma Hausdorff_edist_self : Hausdorff_edist s s = 0 :=
id                                        └─────────────┘   
src                                       └─────────────┘     
typ                                       └─────────────┘   
doc    └──┘                               └─────────────┘
163  begin
st   └─────
164    erw [Hausdorff_edist_def, lattice.sup_idem, ← le_bot_iff],
id          └─────────────────┘  └──────────────┘    └────────┘
src    └───┘└─────────────────┘└┘└──────────────┘└──┘└────────┘
typ    └───┘└─────────────────┘└┘└──────────────┘└──┘└────────┘
doc    └───┘                   └┘                └──┘          
txt    └───┘                   └┘                └──┘          
par    └───┘                   └┘                └──┘          
pid       └┘                   └┘                └──┘          
st   ─────────────────────────┘└────────────────┘└────────────┘└──
165    apply Sup_le _,
id           └────┘
src    └────┘└────┘└┘
typ    └────┘└────┘└┘
doc    └────┘      └┘
txt    └────┘      └┘
par    └────┘      └┘
pid               └┘
st   ───────────────┘└─
166    simp [le_bot_iff, inf_edist_zero_of_mem] {contextual := tt},
id           └────────┘  └───────────────────┘                 └┘
src    └────┘└────────┘└┘└───────────────────┘└┘ └────────────┘└┘
typ    └────┘└────────┘└┘└───────────────────┘└┘ └────────────┘└┘
doc    └────┘          └┘└───────────────────┘└┘ └────────────┘  
txt    └────┘          └┘                     └┘ └────────────┘  
par    └────┘          └┘                     └┘ └────────────┘  
pid                  └┘                      └────────────┘  
st   ────────────────────────────────────────────────────────────┘└─
167  end
st   ──┘
168  
169  /-- The Haudorff edistances of `s` to `t` and of `t` to `s` coincide -/
170  lemma Hausdorff_edist_comm : Hausdorff_edist s t = Hausdorff_edist t s :=
id                                └─────────────┘    └─────────────┘  
src                               └─────────────┘      └─────────────┘
typ                               └─────────────┘    └─────────────┘  
doc                               └─────────────┘       └─────────────┘
171  by unfold Hausdorff_edist; apply sup_comm
id                                    └──────┘
src     └────────────────────┘  └────┘└──────┘
typ     └────────────────────┘  └────┘└──────┘
doc     └────────────────────┘  └────┘        
txt     └────────────────────┘  └────┘        
par     └────────────────────┘  └────┘        
pid           └──────────────┘               
st     └───────────────────────────────────────
172  
src  
typ  
doc  
txt  
par  
pid  
st   
173  /-- Bounding the Hausdorff edistance by bounding the edistance of any point
174  in each set to the other set -/
175  lemma Hausdorff_edist_le_of_inf_edist {r : ennreal}
id                                              └─────┘
src                                             └─────┘
typ                                             └─────┘
doc                                             └─────┘
176    (H1 : ∀x ∈ s, inf_edist x t ≤ r) (H2 : ∀x ∈ t, inf_edist x s ≤ r) :
id                 └───────┘                  └───────┘    
src                  └───────┘                       └───────┘     
typ                └───────┘                  └───────┘    
doc                  └───────┘                        └───────┘
177    Hausdorff_edist s t ≤ r :=
id     └─────────────┘    
src    └─────────────┘     
typ    └─────────────┘    
doc    └─────────────┘
178  begin
st   └─────
179    simp only [Hausdorff_edist, -mem_image, set.ball_image_iff, lattice.Sup_le_iff, lattice.sup_le_iff],
id                └─────────────┘              └────────────────┘  └────────────────┘  └────────────────┘
src    └─────────┘└─────────────┘└────────────┘└────────────────┘└┘└────────────────┘└┘└────────────────┘
typ    └─────────┘└─────────────┘└────────────┘└────────────────┘└┘└────────────────┘└┘└────────────────┘
doc    └─────────┘└─────────────┘└────────────┘                  └┘                  └┘                  
txt    └─────────┘               └────────────┘                  └┘                  └┘                  
par    └─────────┘               └────────────┘                  └┘                  └┘                  
pid        └──┘└┘               └────────────┘                  └┘                  └┘                  
st   ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
180    exact ⟨H1, H2⟩
id            └┘  └┘
src    └────┘   └┘  └┘
typ    └────┘ └┘└┘└┘└┘
doc    └────┘   └┘  └┘
txt    └────┘   └┘  └┘
par    └────┘   └┘  └┘
pid            └┘  
st   ────────────────┘
181  end
st   └─┘
182  
183  /-- Bounding the Hausdorff edistance by exhibiting, for any point in each set,
184  another point in the other set at controlled distance -/
185  lemma Hausdorff_edist_le_of_mem_edist {r : ennreal}
id                                              └─────┘
src                                             └─────┘
typ                                             └─────┘
doc                                             └─────┘
186    (H1 : ∀x ∈ s, ∃y ∈ t, edist x y ≤ r) (H2 : ∀x ∈ t, ∃y ∈ s, edist x y ≤ r) :
id                     └───┘                      └───┘    
src                        └───┘                             └───┘     
typ                    └───┘                      └───┘    
187    Hausdorff_edist s t ≤ r :=
id     └─────────────┘    
src    └─────────────┘     
typ    └─────────────┘    
doc    └─────────────┘
188  begin
st   └─────
189    refine Hausdorff_edist_le_of_inf_edist _ _,
id            └─────────────────────────────┘
src    └─────┘└─────────────────────────────┘└──┘
typ    └─────┘└─────────────────────────────┘└──┘
doc    └─────┘└─────────────────────────────┘└──┘
txt    └─────┘                               └──┘
par    └─────┘                               └──┘
pid                                         └──┘
st   ───────────────────────────────────────────┘└─
190    { assume x xs,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
191      rcases H1 x xs with ⟨y, yt, hy⟩,
id              └┘  └┘
src      └─────┘     └───────────────┘
typ      └─────┘└┘└┘└───────────────┘
doc      └─────┘     └───────────────┘
txt      └─────┘     └───────────────┘
par      └─────┘     └───────────────┘
pid                 └───────────────┘
st   ──────────────────────────────────┘└─
192      exact le_trans (inf_edist_le_edist_of_mem yt) hy },
id             └──────┘  └───────────────────────┘ └┘  └┘
src      └────┘└──────┘ └───────────────────────┘  └┘  
typ      └────┘└──────┘ └───────────────────────┘└┘└┘└┘
doc      └────┘         └───────────────────────┘  └┘  
txt      └────┘                                    └┘  
par      └────┘                                    └┘  
pid                                               └┘  
st   ────────────────────────────────────────────────────┘└┘
193    { assume x xt,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ──────────────┘└─
194      rcases H2 x xt with ⟨y, ys, hy⟩,
id              └┘  └┘
src      └─────┘     └───────────────┘
typ      └─────┘└┘└┘└───────────────┘
doc      └─────┘     └───────────────┘
txt      └─────┘     └───────────────┘
par      └─────┘     └───────────────┘
pid                 └───────────────┘
st   ──────────────────────────────────┘└─
195      exact le_trans (inf_edist_le_edist_of_mem ys) hy }
id             └──────┘  └───────────────────────┘ └┘  └┘
src      └────┘└──────┘ └───────────────────────┘  └┘  
typ      └────┘└──────┘ └───────────────────────┘└┘└┘└┘
doc      └────┘         └───────────────────────┘  └┘  
txt      └────┘                                    └┘  
par      └────┘                                    └┘  
pid                                               └┘  
st   ────────────────────────────────────────────────────┘└─
196  end
st   ──┘
197  
198  /-- The distance to a set is controlled by the Hausdorff distance -/
199  lemma inf_edist_le_Hausdorff_edist_of_mem (h : x ∈ s) : inf_edist x t ≤ Hausdorff_edist s t :=
id                                                        └───────┘    └─────────────┘  
src                                                         └───────┘      └─────────────┘
typ                                                       └───────┘    └─────────────┘  
doc                                                          └───────┘       └─────────────┘
200  begin
st   └─────
201    rw Hausdorff_edist_def,
id        └─────────────────┘
src    └─┘└─────────────────┘
typ    └─┘└─────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────────────────┘└─
202    refine le_trans (le_Sup _) le_sup_left,
id            └──────┘  └────┘    └─────────┘
src    └─────┘└──────┘ └────┘└──┘└─────────┘
typ    └─────┘└──────┘ └────┘└──┘└─────────┘
doc    └─────┘               └──┘
txt    └─────┘               └──┘
par    └─────┘               └──┘
pid                         └──┘
st   ───────────────────────────────────────┘└─
203    exact mem_image_of_mem _ h
id           └──────────────┘   
src    └────┘└──────────────┘└─┘ 
typ    └────┘└──────────────┘└─┘
doc    └────┘                └─┘ 
txt    └────┘                └─┘ 
par    └────┘                └─┘ 
pid                         └─┘ 
st   ────────────────────────────┘
204  end
st   └─┘
205  
206  /-- If the Hausdorff distance is `<r`, then any point in one of the sets has
207  a corresponding point at distance `<r` in the other set -/
208  lemma exists_edist_lt_of_Hausdorff_edist_lt {r : ennreal} (h : x ∈ s) (H : Hausdorff_edist s t < r) :
id                                                    └─────┘                └─────────────┘    
src                                                   └─────┘                  └─────────────┘     
typ                                                   └─────┘                └─────────────┘    
doc                                                   └─────┘                   └─────────────┘
209    ∃y∈t, edist x y < r :=
id       └───┘    
src        └───┘     
typ      └───┘    
210  exists_edist_lt_of_inf_edist_lt $ calc
id   └─────────────────────────────┘
src  └─────────────────────────────┘
typ  └─────────────────────────────┘
doc  └─────────────────────────────┘
211    inf_edist x t ≤ Sup ((λx, inf_edist x t) '' s) : le_Sup (mem_image_of_mem _ h)
id     └───────┘     └─┘      └───────┘    └┘     └────┘  └──────────────┘   
src    └───────┘       └─┘       └───────┘      └┘      └────┘  └──────────────┘
typ    └───────┘     └─┘      └───────┘    └┘     └────┘  └──────────────┘   
doc    └───────┘       └─┘       └───────┘
212    ... ≤ Sup ((λx, inf_edist x t) '' s) ⊔ Sup ((λx, inf_edist x s) '' t) : le_sup_left
id           └─┘      └───────┘    └┘    └─┘      └───────┘    └┘     └─────────┘
src          └─┘       └───────┘      └┘     └─┘       └───────┘      └┘      └─────────┘
typ          └─┘      └───────┘    └┘    └─┘      └───────┘    └┘     └─────────┘
doc          └─┘       └───────┘              └─┘       └───────┘
213    ... < r : by rwa Hausdorff_edist_def at H
id                     └─────────────────┘
src                 └──┘└─────────────────┘└─────
typ                └──┘└─────────────────┘└─────
doc                 └──┘                   └─────
txt                 └──┘                   └─────
par                 └──┘                   └─────
pid                                       └───┘
st                 └─────────────────────────────
214  
src  
typ  
doc  
txt  
par  
pid  
st   
215  /-- The distance from `x` to `s`or `t` is controlled in terms of the Hausdorff distance
216  between `s` and `t` -/
217  lemma inf_edist_le_inf_edist_add_Hausdorff_edist :
218    inf_edist x t ≤ inf_edist x s + Hausdorff_edist s t :=
id     └───────┘    └───────┘    └─────────────┘  
src    └───────┘      └───────┘      └─────────────┘
typ    └───────┘    └───────┘    └─────────────┘  
doc    └───────┘       └───────┘       └─────────────┘
219  ennreal.le_of_forall_epsilon_le $ λε εpos h, begin
id   └─────────────────────────────┘     └──┘ 
src  └─────────────────────────────┘
typ  └─────────────────────────────┘     └──┘ 
st                                                └─────
220    have εpos' : (0 : ennreal) < ε := by simpa,
id                       └─────┘   
src    └───────────┘ └──┘└─────┘└┘ └──┘  └───┘
typ    └───────────┘ └──┘└─────┘└┘└──┘  └───┘
doc    └───────────┘ └──┘└─────┘└┘  └──┘  └───┘
txt    └───────────┘ └──┘       └┘  └──┘  └───┘
par    └───────────┘ └──┘       └┘  └──┘  └───┘
pid    └────────┘└─┘ └──┘       └┘  └──┘  └────┘
st   ─────────────────────────────────────┘└────┘└─
221    have : inf_edist x s < inf_edist x s + ε/2 :=
id                            └───────┘    
src    └─────┘            └───────┘   └────
typ    └─────┘            └───────┘└────
doc    └─────┘            └───────┘     └────
txt    └─────┘                          └────
par    └─────┘                          └────
pid    └───┘└┘                          └────
st   ────────────────────────────────────────────────
222      ennreal.lt_add_right (ennreal.add_lt_top.1 h).1 (ennreal.half_pos εpos'),
id       └──────────────────┘  └────────────────┘        └──────────────┘ └───┘
src  ───┘└──────────────────┘ └────────────────┘└─┘ └──┘ └──────────────┘     
typ  ───┘└──────────────────┘ └────────────────┘└─┘└──┘ └──────────────┘└───┘
doc  ───┘                                       └─┘ └──┘                      
txt  ───┘                                       └─┘ └──┘                      
par  ───┘                                       └─┘ └──┘                      
pid  ───┘                                       └─┘ └──┘                      
st   ───────────────────────────────────────────────────────────────────────────┘└─
223    rcases exists_edist_lt_of_inf_edist_lt this with ⟨y, ys, dxy⟩,
id            └─────────────────────────────┘ └──┘
src    └─────┘└─────────────────────────────┘    └────────────────┘
typ    └─────┘└─────────────────────────────┘└──┘└────────────────┘
doc    └─────┘└─────────────────────────────┘    └────────────────┘
txt    └─────┘                                   └────────────────┘
par    └─────┘                                   └────────────────┘
pid                                             └────────────────┘
st   ──────────────────────────────────────────────────────────────┘└─
224    -- y : α,  ys : y ∈ s,  dxy : edist x y < inf_edist x s + ↑ε / 2
st   ───────────────────────────────────────────────────────────────────
225    have : Hausdorff_edist s t < Hausdorff_edist s t + ε/2 :=
id                                  └─────────────┘     
src    └─────┘                  └─────────────┘     └────
typ    └─────┘                  └─────────────┘  └────
doc    └─────┘                  └─────────────┘     └────
txt    └─────┘                                      └────
par    └─────┘                                      └────
pid    └───┘└┘                                      └────
st   ────────────────────────────────────────────────────────────
226      ennreal.lt_add_right (ennreal.add_lt_top.1 h).2 (ennreal.half_pos εpos'),
id       └──────────────────┘  └────────────────┘        └──────────────┘ └───┘
src  ───┘└──────────────────┘ └────────────────┘└─┘ └──┘ └──────────────┘     
typ  ───┘└──────────────────┘ └────────────────┘└─┘└──┘ └──────────────┘└───┘
doc  ───┘                                       └─┘ └──┘                      
txt  ───┘                                       └─┘ └──┘                      
par  ───┘                                       └─┘ └──┘                      
pid  ───┘                                       └─┘ └──┘                      
st   ───────────────────────────────────────────────────────────────────────────┘└─
227    rcases exists_edist_lt_of_Hausdorff_edist_lt ys this with ⟨z, zt, dyz⟩,
id            └───────────────────────────────────┘ └┘ └──┘
src    └─────┘└───────────────────────────────────┘      └────────────────┘
typ    └─────┘└───────────────────────────────────┘└┘└──┘└────────────────┘
doc    └─────┘└───────────────────────────────────┘      └────────────────┘
txt    └─────┘                                           └────────────────┘
par    └─────┘                                           └────────────────┘
pid                                                     └────────────────┘
st   ───────────────────────────────────────────────────────────────────────┘└─
228    -- z : α,  zt : z ∈ t,  dyz : edist y z < Hausdorff_edist s t + ↑ε / 2
st   ─────────────────────────────────────────────────────────────────────────
229    calc inf_edist x t ≤ edist x z : inf_edist_le_edist_of_mem zt
id     └──┘                 └───┘     └───────────────────────┘ └┘
src    └──┘                 └───┘       └───────────────────────┘
typ    └──┘                 └───┘     └───────────────────────┘ └┘
doc    └──┘                             └───────────────────────┘
st   ────────────────────────────────────────────────────────────────
230      ... ≤ edist x y + edist y z : edist_triangle _ _ _
id                                    └────────────┘
src                                    └────────────┘
typ                                   └────────────┘
st   ───────────────────────────────────────────────────────
231      ... ≤ (inf_edist x s + ε/2) + (Hausdorff_edist s t + ε/2) : add_le_add' (le_of_lt dxy) (le_of_lt dyz)
id                                                                   └─────────┘           └─┘   └──────┘ └─┘
src                                                                  └─────────┘                 └──────┘
typ                                                                  └─────────┘           └─┘   └──────┘ └─┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────────
232      ... = inf_edist x s + Hausdorff_edist s t + ε : by simp [ennreal.add_halves, add_comm]
id             └───────┘       └─────────────┘                 └────────────────┘  └──────┘
src            └───────┘       └─────────────┘              └────┘└────────────────┘└┘└──────┘└┘
typ            └───────┘       └─────────────┘           └────┘└────────────────┘└┘└──────┘└┘
doc            └───────┘       └─────────────┘              └────┘                  └┘        └┘
txt                                                         └────┘                  └┘        └┘
par                                                         └────┘                  └┘        └┘
pid                                                                               └┘        
st   ─────────────────────────────────────────────────────┘└───────────────────────────────────┘
233  end
st   └─┘
234  
235  /-- The Hausdorff edistance is invariant under eisometries -/
236  lemma Hausdorff_edist_image (h : isometry Φ) :
id                                    └──────┘ 
src                                   └──────┘
typ                                   └──────┘ 
doc                                   └──────┘
237    Hausdorff_edist (Φ '' s) (Φ '' t) = Hausdorff_edist s t :=
id     └─────────────┘   └┘     └┘    └─────────────┘  
src    └─────────────┘    └┘       └┘     └─────────────┘
typ    └─────────────┘   └┘     └┘    └─────────────┘  
doc    └─────────────┘                     └─────────────┘
238  begin
st   └─────
239    unfold Hausdorff_edist,
src    └────────────────────┘
typ    └────────────────────┘
doc    └────────────────────┘
txt    └────────────────────┘
par    └────────────────────┘
pid          └──────────────┘
st   ───────────────────────┘└─
240    congr,
src    └───┘
typ    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
241    { ext b,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid         └┘
st   ───┘└───┘└─
242      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
243      { assume hb,
src        └───────┘
typ        └───────┘
doc        └───────┘
txt        └───────┘
par        └───────┘
pid        └───────┘
st   ─────┘└───────┘└─
244        rcases (mem_image _ _ _ ).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
id                 └───────┘           └┘
src        └─────┘ └───────┘└─────────┘  └──────────────────┘
typ        └─────┘ └───────┘└─────────┘└┘└──────────────────┘
doc        └─────┘          └─────────┘  └──────────────────┘
txt        └─────┘          └─────────┘  └──────────────────┘
par        └─────┘          └─────────┘  └──────────────────┘
pid                        └─────────┘  └──────────────────┘
st   ───────────────────────────────────────────────────────┘└─
245        rcases (mem_image _ _ _ ).1 hy with ⟨z, ⟨hz, hz'⟩⟩,
id                 └───────┘           └┘
src        └─────┘ └───────┘└─────────┘  └──────────────────┘
typ        └─────┘ └───────┘└─────────┘└┘└──────────────────┘
doc        └─────┘          └─────────┘  └──────────────────┘
txt        └─────┘          └─────────┘  └──────────────────┘
par        └─────┘          └─────────┘  └──────────────────┘
pid                        └─────────┘  └──────────────────┘
st   ───────────────────────────────────────────────────────┘└─
246        rw [← hy', ← hz', inf_edist_image h],
id               └─┘    └─┘  └─────────────┘ 
src        └────┘   └──┘   └┘└─────────────┘ 
typ        └────┘└─┘└──┘└─┘└┘└─────────────┘
doc        └────┘   └──┘   └┘└─────────────┘ 
txt        └────┘   └──┘   └┘                
par        └────┘   └──┘   └┘                
pid          └──┘   └──┘   └┘                
st   ──────────────┘└─────┘└─────────────────┘└──
247        exact mem_image_of_mem _ hz },
id               └──────────────┘   └┘
src        └────┘└──────────────┘└─┘  
typ        └────┘└──────────────┘└─┘└┘
doc        └────┘                └─┘  
txt        └────┘                └─┘  
par        └────┘                └─┘  
pid                             └─┘  
st   ─────────────────────────────────┘└┘
248      { assume hb,
src        └───────┘
typ        └───────┘
doc        └───────┘
txt        └───────┘
par        └───────┘
pid        └───────┘
st   ──────────────┘└─
249        rcases (mem_image _ _ _ ).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
id                 └───────┘           └┘
src        └─────┘ └───────┘└─────────┘  └──────────────────┘
typ        └─────┘ └───────┘└─────────┘└┘└──────────────────┘
doc        └─────┘          └─────────┘  └──────────────────┘
txt        └─────┘          └─────────┘  └──────────────────┘
par        └─────┘          └─────────┘  └──────────────────┘
pid                        └─────────┘  └──────────────────┘
st   ───────────────────────────────────────────────────────┘└─
250        rw [← hy', ← inf_edist_image h],
id               └─┘    └─────────────┘ 
src        └────┘   └──┘└─────────────┘ 
typ        └────┘└─┘└──┘└─────────────┘
doc        └────┘   └──┘└─────────────┘ 
txt        └────┘   └──┘                
par        └────┘   └──┘                
pid          └──┘   └──┘                
st   ──────────────┘└───────────────────┘└──
251        exact mem_image_of_mem _ (mem_image_of_mem _ hy) }},
id                                   └──────────────┘   └┘
src        └────┘                └─┘ └──────────────┘└─┘  └┘
typ        └────┘                └─┘ └──────────────┘└─┘└┘└┘
doc        └────┘                └─┘                 └─┘  └┘
txt        └────┘                └─┘                 └─┘  └┘
par        └────┘                └─┘                 └─┘  └┘
pid                             └─┘                 └─┘  
st   ──────────────────────────────────────────────────────┘└─┘
252    { ext b,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid         └┘
st   ────────┘└─
253      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
254      { assume hb,
src        └───────┘
typ        └───────┘
doc        └───────┘
txt        └───────┘
par        └───────┘
pid        └───────┘
st   ─────┘└───────┘└─
255        rcases (mem_image _ _ _ ).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
id                 └───────┘           └┘
src        └─────┘ └───────┘└─────────┘  └──────────────────┘
typ        └─────┘ └───────┘└─────────┘└┘└──────────────────┘
doc        └─────┘          └─────────┘  └──────────────────┘
txt        └─────┘          └─────────┘  └──────────────────┘
par        └─────┘          └─────────┘  └──────────────────┘
pid                        └─────────┘  └──────────────────┘
st   ───────────────────────────────────────────────────────┘└─
256        rcases (mem_image _ _ _ ).1 hy with ⟨z, ⟨hz, hz'⟩⟩,
id                 └───────┘           └┘
src        └─────┘ └───────┘└─────────┘  └──────────────────┘
typ        └─────┘ └───────┘└─────────┘└┘└──────────────────┘
doc        └─────┘          └─────────┘  └──────────────────┘
txt        └─────┘          └─────────┘  └──────────────────┘
par        └─────┘          └─────────┘  └──────────────────┘
pid                        └─────────┘  └──────────────────┘
st   ───────────────────────────────────────────────────────┘└─
257        rw [← hy', ← hz', inf_edist_image h],
id               └─┘    └─┘  └─────────────┘ 
src        └────┘   └──┘   └┘└─────────────┘ 
typ        └────┘└─┘└──┘└─┘└┘└─────────────┘
doc        └────┘   └──┘   └┘└─────────────┘ 
txt        └────┘   └──┘   └┘                
par        └────┘   └──┘   └┘                
pid          └──┘   └──┘   └┘                
st   ──────────────┘└─────┘└─────────────────┘└──
258        exact mem_image_of_mem _ hz },
id               └──────────────┘   └┘
src        └────┘└──────────────┘└─┘  
typ        └────┘└──────────────┘└─┘└┘
doc        └────┘                └─┘  
txt        └────┘                └─┘  
par        └────┘                └─┘  
pid                             └─┘  
st   ─────────────────────────────────┘└┘
259      { assume hb,
src        └───────┘
typ        └───────┘
doc        └───────┘
txt        └───────┘
par        └───────┘
pid        └───────┘
st   ──────────────┘└─
260        rcases (mem_image _ _ _ ).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
id                 └───────┘           └┘
src        └─────┘ └───────┘└─────────┘  └──────────────────┘
typ        └─────┘ └───────┘└─────────┘└┘└──────────────────┘
doc        └─────┘          └─────────┘  └──────────────────┘
txt        └─────┘          └─────────┘  └──────────────────┘
par        └─────┘          └─────────┘  └──────────────────┘
pid                        └─────────┘  └──────────────────┘
st   ───────────────────────────────────────────────────────┘└─
261        rw [← hy', ← inf_edist_image h],
id               └─┘    └─────────────┘ 
src        └────┘   └──┘└─────────────┘ 
typ        └────┘└─┘└──┘└─────────────┘
doc        └────┘   └──┘└─────────────┘ 
txt        └────┘   └──┘                
par        └────┘   └──┘                
pid          └──┘   └──┘                
st   ──────────────┘└───────────────────┘└──
262        exact mem_image_of_mem _ (mem_image_of_mem _ hy) }}
id                                   └──────────────┘   └┘
src        └────┘                └─┘ └──────────────┘└─┘  └┘
typ        └────┘                └─┘ └──────────────┘└─┘└┘└┘
doc        └────┘                └─┘                 └─┘  └┘
txt        └────┘                └─┘                 └─┘  └┘
par        └────┘                └─┘                 └─┘  └┘
pid                             └─┘                 └─┘  
st   ──────────────────────────────────────────────────────┘└──
263  end
st   ──┘
264  
265  /-- The Hausdorff distance is controlled by the diameter of the union -/
266  lemma Hausdorff_edist_le_ediam (hs : s.nonempty) (ht : t.nonempty) : Hausdorff_edist s t ≤ diam (s ∪ t) :=
id                                        └───────┘        └───────┘    └─────────────┘    └──┘    
src                                        └───────┘         └───────┘    └─────────────┘      └──┘    
typ                                       └───────┘        └───────┘    └─────────────┘    └──┘    
doc                                        └───────┘         └───────┘    └─────────────┘       └──┘
267  begin
st   └─────
268    rcases hs with ⟨x, xs⟩,
id            └┘
src    └─────┘  └───────────┘
typ    └─────┘└┘└───────────┘
doc    └─────┘  └───────────┘
txt    └─────┘  └───────────┘
par    └─────┘  └───────────┘
pid            └───────────┘
st   ───────────────────────┘└─
269    rcases ht with ⟨y, yt⟩,
id            └┘
src    └─────┘  └───────────┘
typ    └─────┘└┘└───────────┘
doc    └─────┘  └───────────┘
txt    └─────┘  └───────────┘
par    └─────┘  └───────────┘
pid            └───────────┘
st   ───────────────────────┘└─
270    refine Hausdorff_edist_le_of_mem_edist _ _,
id            └─────────────────────────────┘
src    └─────┘└─────────────────────────────┘└──┘
typ    └─────┘└─────────────────────────────┘└──┘
doc    └─────┘└─────────────────────────────┘└──┘
txt    └─────┘                               └──┘
par    └─────┘                               └──┘
pid                                         └──┘
st   ───────────────────────────────────────────┘└─
271    { exact λz hz, ⟨y, yt, edist_le_diam_of_mem (subset_union_left _ _ hz) (subset_union_right _ _ yt)⟩ },
id                           └──────────────────┘  └───────────────┘          └────────────────┘     └┘
src      └────┘ └────┘  └┘  └┘└──────────────────┘ └───────────────┘└───┘  └┘ └────────────────┘└───┘  └─┘
typ      └────┘ └────┘ └┘  └┘└──────────────────┘ └───────────────┘└───┘  └┘ └────────────────┘└───┘└┘└─┘
doc      └────┘ └────┘  └┘  └┘└──────────────────┘                  └───┘  └┘                   └───┘  └─┘
txt      └────┘ └────┘  └┘  └┘                                      └───┘  └┘                   └───┘  └─┘
par      └────┘ └────┘  └┘  └┘                                      └───┘  └┘                   └───┘  └─┘
pid            └────┘  └┘  └┘                                      └───┘  └┘                   └───┘  └┘
st   ───┘└────────────────────────────────────────────────────────────────────────────────────────────────┘└┘
272    { exact λz hz, ⟨x, xs, edist_le_diam_of_mem (subset_union_right _ _ hz) (subset_union_left _ _ xs)⟩ }
id                           └──────────────────┘  └────────────────┘          └───────────────┘     └┘
src      └────┘ └────┘  └┘  └┘└──────────────────┘ └────────────────┘└───┘  └┘ └───────────────┘└───┘  └─┘
typ      └────┘ └────┘ └┘  └┘└──────────────────┘ └────────────────┘└───┘  └┘ └───────────────┘└───┘└┘└─┘
doc      └────┘ └────┘  └┘  └┘└──────────────────┘                   └───┘  └┘                  └───┘  └─┘
txt      └────┘ └────┘  └┘  └┘                                       └───┘  └┘                  └───┘  └─┘
par      └────┘ └────┘  └┘  └┘                                       └───┘  └┘                  └───┘  └─┘
pid            └────┘  └┘  └┘                                       └───┘  └┘                  └───┘  └┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
273  end
st   ──┘
274  
275  /-- The Hausdorff distance satisfies the triangular inequality -/
276  lemma Hausdorff_edist_triangle : Hausdorff_edist s u ≤ Hausdorff_edist s t + Hausdorff_edist t u :=
id                                    └─────────────┘    └─────────────┘    └─────────────┘  
src                                   └─────────────┘      └─────────────┘      └─────────────┘
typ                                   └─────────────┘    └─────────────┘    └─────────────┘  
doc                                   └─────────────┘       └─────────────┘       └─────────────┘
277  begin
st   └─────
278    rw Hausdorff_edist_def,
id        └─────────────────┘
src    └─┘└─────────────────┘
typ    └─┘└─────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────────────────┘└─
279    simp only [and_imp, set.mem_image, lattice.Sup_le_iff, exists_imp_distrib,
id                └─────┘  └───────────┘  └────────────────┘  └────────────────┘
src    └─────────┘└─────┘└┘└───────────┘└┘└────────────────┘└┘└────────────────┘└─
typ    └─────────┘└─────┘└┘└───────────┘└┘└────────────────┘└┘└────────────────┘└─
doc    └─────────┘       └┘             └┘                  └┘                  └─
txt    └─────────┘       └┘             └┘                  └┘                  └─
par    └─────────┘       └┘             └┘                  └┘                  └─
pid        └──┘└┘       └┘             └┘                  └┘                  └─
st   ─────────────────────────────────────────────────────────────────────────────
280               lattice.sup_le_iff, -mem_image, set.ball_image_iff],
id                └────────────────┘              └────────────────┘
src  ────────────┘└────────────────┘└────────────┘└────────────────┘
typ  ────────────┘└────────────────┘└────────────┘└────────────────┘
doc  ────────────┘                  └────────────┘                  
txt  ────────────┘                  └────────────┘                  
par  ────────────┘                  └────────────┘                  
pid  ────────────┘                  └────────────┘                  
st   ───────────────────────────────────────────────────────────────┘└─
281    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
282    show ∀x ∈ s, inf_edist x u ≤ Hausdorff_edist s t + Hausdorff_edist t u, from λx xs, calc
id                  └───────┘                          └─────────────┘  
src    └───┘ └──┘  └───────┘                   └─────────────┘    └───┘ └────┘    
typ    └───┘ └──┘  └───────┘                  └─────────────┘  └───┘ └────┘    
doc    └───┘ └──┘  └───────┘                     └─────────────┘    └───┘ └────┘    
txt    └───┘ └──┘                                                   └───┘ └────┘    
par    └───┘ └──┘                                                   └───┘ └────┘    
pid    └───┘ └──┘                                                   └───┘ └────┘    
st   ───────────────────────────────────────────────────────────────────────────────────────────
283      inf_edist x u ≤ inf_edist x t + Hausdorff_edist t u : inf_edist_le_inf_edist_add_Hausdorff_edist
id                       └───────┘                             └────────────────────────────────────────┘
src  ───┘            └───────┘                    └─┘└────────────────────────────────────────┘
typ  ───┘            └───────┘                    └─┘└────────────────────────────────────────┘
doc  ───┘            └───────┘                    └─┘└────────────────────────────────────────┘
txt  ───┘                                         └─┘                                          
par  ───┘                                         └─┘                                          
pid  ───┘                                         └─┘                                          
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────
284      ... ≤ Hausdorff_edist s t + Hausdorff_edist t u :
id                                  └─────────────┘  
src  ───────┘                   └─────────────┘  └──
typ  ───────┘                  └─────────────┘└──
doc  ───────┘                   └─────────────┘  └──
txt  ───────┘                                    └──
par  ───────┘                                    └──
pid  ───────┘                                    └──
st   ──────────────────────────────────────────────────────
285        add_le_add_right' (inf_edist_le_Hausdorff_edist_of_mem  xs),
id         └───────────────┘  └─────────────────────────────────┘
src  ─────┘└───────────────┘ └─────────────────────────────────┘└┘  
typ  ─────┘└───────────────┘ └─────────────────────────────────┘└┘  
doc  ─────┘                  └─────────────────────────────────┘└┘  
txt  ─────┘                                                     └┘  
par  ─────┘                                                     └┘  
pid  ─────┘                                                     └┘  
st   ────────────────────────────────────────────────────────────────┘└─
286    show ∀x ∈ u, inf_edist x s ≤ Hausdorff_edist s t + Hausdorff_edist t u, from λx xu, calc
id                  └───────┘                            └─────────────┘  
src    └───┘ └──┘  └───────┘                     └─────────────┘    └───┘ └────┘    
typ    └───┘ └──┘  └───────┘                    └─────────────┘  └───┘ └────┘    
doc    └───┘ └──┘  └───────┘                     └─────────────┘    └───┘ └────┘    
txt    └───┘ └──┘                                                   └───┘ └────┘    
par    └───┘ └──┘                                                   └───┘ └────┘    
pid    └───┘ └──┘                                                   └───┘ └────┘    
st   ───────────────────────────────────────────────────────────────────────────────────────────
287      inf_edist x s ≤ inf_edist x t + Hausdorff_edist t s : inf_edist_le_inf_edist_add_Hausdorff_edist
id                       └───────┘       └─────────────┘     └────────────────────────────────────────┘
src  ───┘            └───────┘   └─────────────┘  └─┘└────────────────────────────────────────┘
typ  ───┘            └───────┘   └─────────────┘└─┘└────────────────────────────────────────┘
doc  ───┘            └───────┘   └─────────────┘  └─┘└────────────────────────────────────────┘
txt  ───┘                                         └─┘                                          
par  ───┘                                         └─┘                                          
pid  ───┘                                         └─┘                                          
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────
288      ... ≤ Hausdorff_edist u t + Hausdorff_edist t s :
src  ───────┘                                    └──
typ  ───────┘                                    └──
doc  ───────┘                                    └──
txt  ───────┘                                    └──
par  ───────┘                                    └──
pid  ───────┘                                    └──
st   ──────────────────────────────────────────────────────
289        add_le_add_right' (inf_edist_le_Hausdorff_edist_of_mem xu)
id         └───────────────┘  └─────────────────────────────────┘
src  ─────┘└───────────────┘ └─────────────────────────────────┘  └─
typ  ─────┘└───────────────┘ └─────────────────────────────────┘  └─
doc  ─────┘                  └─────────────────────────────────┘  └─
txt  ─────┘                                                       └─
par  ─────┘                                                       └─
pid  ─────┘                                                       └─
st   ─────────────────────────────────────────────────────────────────
290      ... = Hausdorff_edist s t + Hausdorff_edist t u : by simp [Hausdorff_edist_comm, add_comm]
id                                                                 └──────────────────┘  └──────┘
src  ───────┘                                    └─┘  └────┘└──────────────────┘└┘└──────┘└┘
typ  ───────┘                                   └─┘  └────┘└──────────────────┘└┘└──────┘└┘
doc  ───────┘                                    └─┘  └────┘└──────────────────┘└┘        └┘
txt  ───────┘                                    └─┘  └────┘                    └┘        └┘
par  ───────┘                                    └─┘  └────┘                    └┘        └┘
pid  ───────┘                                    └─┘  └─────┘                    └┘        └┘
st   ───────────────────────────────────────────────────────┘└─────────────────────────────────────┘
291  end
st   └─┘
292  
293  /-- The Hausdorff edistance between a set and its closure vanishes -/
294  @[simp] lemma Hausdorff_edist_self_closure : Hausdorff_edist s (closure s) = 0 :=
id                                                └─────────────┘   └─────┘   
src                                               └─────────────┘    └─────┘    
typ                                               └─────────────┘   └─────┘   
doc    └──┘                                       └─────────────┘    └─────┘
295  begin
st   └─────
296    erw ← le_bot_iff,
id           └────────┘
src    └────┘└────────┘
typ    └────┘└────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid       └─┘
st   ─────────────────┘└─
297    simp only [Hausdorff_edist, inf_edist_closure, -le_zero_iff_eq, and_imp,
id                └─────────────┘  └───────────────┘                   └─────┘
src    └─────────┘└─────────────┘└┘└───────────────┘└─────────────────┘└─────┘└─
typ    └─────────┘└─────────────┘└┘└───────────────┘└─────────────────┘└─────┘└─
doc    └─────────┘└─────────────┘└┘└───────────────┘└─────────────────┘       └─
txt    └─────────┘               └┘                 └─────────────────┘       └─
par    └─────────┘               └┘                 └─────────────────┘       └─
pid        └──┘└┘               └┘                 └─────────────────┘       └─
st   ───────────────────────────────────────────────────────────────────────────
298      set.mem_image, lattice.Sup_le_iff, exists_imp_distrib, lattice.sup_le_iff,
id       └───────────┘  └────────────────┘  └────────────────┘  └────────────────┘
src  ───┘└───────────┘└┘└────────────────┘└┘└────────────────┘└┘└────────────────┘└─
typ  ───┘└───────────┘└┘└────────────────┘└┘└────────────────┘└┘└────────────────┘└─
doc  ───┘             └┘                  └┘                  └┘                  └─
txt  ───┘             └┘                  └┘                  └┘                  └─
par  ───┘             └┘                  └┘                  └┘                  └─
pid  ───┘             └┘                  └┘                  └┘                  └─
st   ───────────────────────────────────────────────────────────────────────────────
299      set.ball_image_iff, ennreal.bot_eq_zero, -mem_image],
id       └────────────────┘  └─────────────────┘
src  ───┘└────────────────┘└┘└─────────────────┘└───────────┘
typ  ───┘└────────────────┘└┘└─────────────────┘└───────────┘
doc  ───┘                  └┘                   └───────────┘
txt  ───┘                  └┘                   └───────────┘
par  ───┘                  └┘                   └───────────┘
pid  ───┘                  └┘                   └───────────┘
st   ───────────────────────────────────────────────────────┘└─
300    simp only [inf_edist_zero_of_mem, mem_closure_iff_inf_edist_zero, le_refl, and_self,
id                └───────────────────┘  └────────────────────────────┘  └─────┘  └──────┘
src    └─────────┘└───────────────────┘└┘└────────────────────────────┘└┘└─────┘└┘└──────┘└─
typ    └─────────┘└───────────────────┘└┘└────────────────────────────┘└┘└─────┘└┘└──────┘└─
doc    └─────────┘└───────────────────┘└┘└────────────────────────────┘└┘       └┘        └─
txt    └─────────┘                     └┘                              └┘       └┘        └─
par    └─────────┘                     └┘                              └┘       └┘        └─
pid        └──┘└┘                     └┘                              └┘       └┘        └─
st   ───────────────────────────────────────────────────────────────────────────────────────
301               forall_true_iff] {contextual := tt}
id                └─────────────┘                 └┘
src  ────────────┘└─────────────┘└┘ └────────────┘└┘└┘
typ  ────────────┘└─────────────┘└┘ └────────────┘└┘└┘
doc  ────────────┘               └┘ └────────────┘  └┘
txt  ────────────┘               └┘ └────────────┘  └┘
par  ────────────┘               └┘ └────────────┘  └┘
pid  ────────────┘                └────────────┘  
st   ────────────────────────────────────────────────┘
302  end
st   └─┘
303  
304  /-- Replacing a set by its closure does not change the Hausdorff edistance. -/
305  @[simp] lemma Hausdorff_edist_closure₁ : Hausdorff_edist (closure s) t = Hausdorff_edist s t :=
id                                            └─────────────┘  └─────┘     └─────────────┘  
src                                           └─────────────┘  └─────┘       └─────────────┘
typ                                           └─────────────┘  └─────┘     └─────────────┘  
doc    └──┘                                   └─────────────┘  └─────┘        └─────────────┘
306  begin
st   └─────
307    refine le_antisymm _ _,
id            └─────────┘
src    └─────┘└─────────┘└──┘
typ    └─────┘└─────────┘└──┘
doc    └─────┘           └──┘
txt    └─────┘           └──┘
par    └─────┘           └──┘
pid                     └──┘
st   ───────────────────────┘└─
308    { calc  _ ≤ Hausdorff_edist (closure s) s + Hausdorff_edist s t : Hausdorff_edist_triangle
id       └──┘                       └─────┘                             └──────────────────────┘
src      └──┘                       └─────┘                             └──────────────────────┘
typ      └──┘                       └─────┘                             └──────────────────────┘
doc      └──┘                       └─────┘                              └──────────────────────┘
st   ───┘└────────────────────────────────────────────────────────────────────────────────────────
309      ... = Hausdorff_edist s t : by simp [Hausdorff_edist_comm] },
id             └─────────────┘              └──────────────────┘
src            └─────────────┘          └────┘└──────────────────┘└┘
typ            └─────────────┘        └────┘└──────────────────┘└┘
doc            └─────────────┘          └────┘└──────────────────┘└┘
txt                                     └────┘                    └┘
par                                     └────┘                    └┘
pid                                                             
st   ─────────────────────────────────┘└───────────────────────────┘└┘
310    { calc _ ≤ Hausdorff_edist s (closure s) + Hausdorff_edist (closure s) t : Hausdorff_edist_triangle
id       └──┘                                                                     └──────────────────────┘
src      └──┘                                                                     └──────────────────────┘
typ      └──┘                                                                     └──────────────────────┘
doc      └──┘                                                                     └──────────────────────┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────
311      ... = Hausdorff_edist (closure s) t : by simp }
id             └─────────────┘  └─────┘   
src            └─────────────┘  └─────┘           └───┘
typ            └─────────────┘  └─────┘         └───┘
doc            └─────────────┘  └─────┘           └───┘
txt                                               └───┘
par                                               └───┘
pid                                                   
st   ───────────────────────────────────────────┘└────┘└─
312  end
st   ──┘
313  
314  /-- Replacing a set by its closure does not change the Hausdorff edistance. -/
315  @[simp] lemma Hausdorff_edist_closure₂ : Hausdorff_edist s (closure t) = Hausdorff_edist s t :=
id                                            └─────────────┘   └─────┘    └─────────────┘  
src                                           └─────────────┘    └─────┘     └─────────────┘
typ                                           └─────────────┘   └─────┘    └─────────────┘  
doc    └──┘                                   └─────────────┘    └─────┘      └─────────────┘
316  by simp [@Hausdorff_edist_comm _ _ s _]
id             └──────────────────┘     
src     └────┘ └──────────────────┘└───┘ └───
typ     └────┘ └──────────────────┘└───┘└───
doc     └────┘ └──────────────────┘└───┘ └───
txt     └────┘                     └───┘ └───
par     └────┘                     └───┘ └───
pid                              └───┘ └─┘
st     └─────────────────────────────────────
317  
src  
typ  
doc  
txt  
par  
pid  
st   
318  /-- The Hausdorff edistance between sets or their closures is the same -/
319  @[simp] lemma Hausdorff_edist_closure : Hausdorff_edist (closure s) (closure t) = Hausdorff_edist s t :=
id                                           └─────────────┘  └─────┘    └─────┘    └─────────────┘  
src                                          └─────────────┘  └─────┘     └─────┘     └─────────────┘
typ                                          └─────────────┘  └─────┘    └─────┘    └─────────────┘  
doc    └──┘                                  └─────────────┘  └─────┘     └─────┘      └─────────────┘
320  by simp
src     └────
typ     └────
doc     └────
txt     └────
par     └────
pid         
st     └─────
321  
src  
typ  
doc  
txt  
par  
pid  
st   
322  /-- Two sets are at zero Hausdorff edistance if and only if they have the same closure -/
323  lemma Hausdorff_edist_zero_iff_closure_eq_closure : Hausdorff_edist s t = 0 ↔ closure s = closure t :=
id                                                       └─────────────┘       └─────┘   └─────┘ 
src                                                      └─────────────┘         └─────┘    └─────┘
typ                                                      └─────────────┘       └─────┘   └─────┘ 
doc                                                      └─────────────┘           └─────┘     └─────┘
324  ⟨begin
st    └─────
325    assume h,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
326    refine subset.antisymm _ _,
id            └─────────────┘
src    └─────┘└─────────────┘└──┘
typ    └─────┘└─────────────┘└──┘
doc    └─────┘               └──┘
txt    └─────┘               └──┘
par    └─────┘               └──┘
pid                         └──┘
st   ───────────────────────────┘└─
327    { have : s ⊆ closure t := λx xs, mem_closure_iff_inf_edist_zero.2 $ begin
id                └─────┘            └────────────────────────────┘
src      └─────┘ └─────┘ └──┘ └────┘└────────────────────────────┘└─┘      
typ      └─────┘└─────┘└──┘ └────┘└────────────────────────────┘└─┘      
doc      └─────┘  └─────┘ └──┘ └────┘└────────────────────────────┘└─┘      
txt      └─────┘          └──┘ └────┘                              └─┘      
par      └─────┘          └──┘ └────┘                              └─┘      
pid      └───┘└┘          └──┘ └────┘                              └─┘      
st   ───┘└────────────────────────────────────────────────────────────────┘└─────
328        erw ← le_bot_iff,
id               └────────┘
src  ─────┘└────┘└────────┘└─
typ  ─────┘└────┘└────────┘└─
doc  ─────┘└────┘          └─
txt  ─────┘└────┘          └─
par  ─────┘└────┘          └─
pid  ───────────┘          └─
st   ─────────────────────┘└─
329        have := @inf_edist_le_Hausdorff_edist_of_mem _ _ _ _ t xs,
id                  └─────────────────────────────────┘          └┘
src  ─────────────┘ └─────────────────────────────────┘└───────┘   └─
typ  ─────────────┘ └─────────────────────────────────┘└───────┘└┘└─
doc  ─────────────┘ └─────────────────────────────────┘└───────┘   └─
txt  ─────────────┘                                    └───────┘   └─
par  ─────────────┘                                    └───────┘   └─
pid  ─────────────┘                                    └───────┘   └─
st   ──────────────────────────────────────────────────────────────┘└─
330        rwa h at this,
id             
src  ─────┘└──┘ └──────┘└─
typ  ─────┘└──┘└──────┘└─
doc  ─────┘└──┘ └──────┘└─
txt  ─────┘└──┘ └──────┘└─
par  ─────┘└──┘ └──────┘└─
pid  ─────────┘ └─────────
st   ──────────────────┘└─
331      end,
src  ──────┘
typ  ──────┘
doc  ──────┘
txt  ──────┘
par  ──────┘
pid  ──────┘
st   ──────┘
332      by rw ← @closure_closure _ _ t; exact closure_mono this },
id                └─────────────┘             └──────────┘ └──┘
src         └───┘ └─────────────┘└───┘   └────┘└──────────┘    
typ         └───┘ └─────────────┘└───┘  └────┘└──────────┘└──┘
doc         └───┘                └───┘   └────┘                
txt         └───┘                └───┘   └────┘                
par         └───┘                └───┘   └────┘                
pid           └─┘                └───┘                        
st                                                               └┘
333    { have : t ⊆ closure s := λx xt, mem_closure_iff_inf_edist_zero.2 $ begin
id                 └─────┘            └────────────────────────────┘
src      └─────┘  └─────┘ └──┘ └────┘└────────────────────────────┘└─┘      
typ      └─────┘ └─────┘└──┘ └────┘└────────────────────────────┘└─┘      
doc      └─────┘  └─────┘ └──┘ └────┘└────────────────────────────┘└─┘      
txt      └─────┘          └──┘ └────┘                              └─┘      
par      └─────┘          └──┘ └────┘                              └─┘      
pid      └───┘└┘          └──┘ └────┘                              └─┘      
st   ─────────────────────────────────────────────────────────────────────┘└─────
334        erw ← le_bot_iff,
id               └────────┘
src  ─────┘└────┘└────────┘└─
typ  ─────┘└────┘└────────┘└─
doc  ─────┘└────┘          └─
txt  ─────┘└────┘          └─
par  ─────┘└────┘          └─
pid  ───────────┘          └─
st   ─────────────────────┘└─
335        have := @inf_edist_le_Hausdorff_edist_of_mem _ _ _ _ s xt,
id                  └─────────────────────────────────┘          └┘
src  ─────────────┘ └─────────────────────────────────┘└───────┘   └─
typ  ─────────────┘ └─────────────────────────────────┘└───────┘└┘└─
doc  ─────────────┘ └─────────────────────────────────┘└───────┘   └─
txt  ─────────────┘                                    └───────┘   └─
par  ─────────────┘                                    └───────┘   └─
pid  ─────────────┘                                    └───────┘   └─
st   ──────────────────────────────────────────────────────────────┘└─
336        rw Hausdorff_edist_comm at h,
id            └──────────────────┘
src  ─────┘└─┘└──────────────────┘└───┘└─
typ  ─────┘└─┘└──────────────────┘└───┘└─
doc  ─────┘└─┘└──────────────────┘└───┘└─
txt  ─────┘└─┘                    └───┘└─
par  ─────┘└─┘                    └───┘└─
pid  ────────┘                    └──────
st   ─────────────────────────────────┘└─
337        rwa h at this,
id             
src  ─────┘└──┘ └──────┘└─
typ  ─────┘└──┘└──────┘└─
doc  ─────┘└──┘ └──────┘└─
txt  ─────┘└──┘ └──────┘└─
par  ─────┘└──┘ └──────┘└─
pid  ─────────┘ └─────────
st   ──────────────────┘└─
338      end,
src  ──────┘
typ  ──────┘
doc  ──────┘
txt  ──────┘
par  ──────┘
pid  ──────┘
st   ──────┘
339      by rw ← @closure_closure _ _ s; exact closure_mono this }
id                └─────────────┘             └──────────┘ └──┘
src         └───┘ └─────────────┘└───┘   └────┘└──────────┘    
typ         └───┘ └─────────────┘└───┘  └────┘└──────────┘└──┘
doc         └───┘                └───┘   └────┘                
txt         └───┘                └───┘   └────┘                
par         └───┘                └───┘   └────┘                
pid           └─┘                └───┘                        
st                                                               └─
340  end,
st   ──┘
341  λh, by rw [← Hausdorff_edist_closure, h, Hausdorff_edist_self]⟩
id               └─────────────────────┘    └──────────────────┘
src         └────┘└─────────────────────┘└┘ └┘└──────────────────┘
typ        └────┘└─────────────────────┘└┘└┘└──────────────────┘
doc         └────┘└─────────────────────┘└┘ └┘└──────────────────┘
txt         └────┘                       └┘ └┘                    
par         └────┘                       └┘ └┘                    
pid           └──┘                       └┘ └┘                    
st         └────────────────────────────┘└─┘└────────────────────┘
342  
343  /-- Two closed sets are at zero Hausdorff edistance if and only if they coincide -/
344  lemma Hausdorff_edist_zero_iff_eq_of_closed (hs : is_closed s) (ht : is_closed t) :
id                                                     └───────┘         └───────┘ 
src                                                    └───────┘          └───────┘
typ                                                    └───────┘         └───────┘ 
doc                                                    └───────┘          └───────┘
345    Hausdorff_edist s t = 0 ↔ s = t :=
id     └─────────────┘         
src    └─────────────┘           
typ    └─────────────┘         
doc    └─────────────┘
346  by rw [Hausdorff_edist_zero_iff_closure_eq_closure, closure_eq_iff_is_closed.2 hs,
id          └─────────────────────────────────────────┘  └──────────────────────┘   └┘
src     └──┘└─────────────────────────────────────────┘└┘└──────────────────────┘└─┘  └─
typ     └──┘└─────────────────────────────────────────┘└┘└──────────────────────┘└─┘└┘└─
doc     └──┘└─────────────────────────────────────────┘└┘                        └─┘  └─
txt     └──┘                                           └┘                        └─┘  └─
par     └──┘                                           └┘                        └─┘  └─
pid       └┘                                           └┘                        └─┘  └─
st     └──────────────────────────────────────────────┘└─────────────────────────────┘└─
347         closure_eq_iff_is_closed.2 ht]
id          └──────────────────────┘   └┘
src  ──────┘└──────────────────────┘└─┘  └─
typ  ──────┘└──────────────────────┘└─┘└┘└─
doc  ──────┘                        └─┘  └─
txt  ──────┘                        └─┘  └─
par  ──────┘                        └─┘  └─
pid  ──────┘                        └─┘  
st   ───────────────────────────────────┘
348  
src  
typ  
doc  
txt  
par  
pid  
st   
349  /-- The Haudorff edistance to the empty set is infinite -/
350  lemma Hausdorff_edist_empty (ne : s.nonempty) : Hausdorff_edist s ∅ = ∞ :=
id                                     └───────┘    └─────────────┘    
src                                     └───────┘    └─────────────┘     
typ                                    └───────┘    └─────────────┘    
doc                                     └───────┘    └─────────────┘       
351  begin
st   └─────
352    rcases ne with ⟨x, xs⟩,
id            └┘
src    └─────┘└┘└───────────┘
typ    └─────┘└┘└───────────┘
doc    └─────┘  └───────────┘
txt    └─────┘  └───────────┘
par    └─────┘  └───────────┘
pid            └───────────┘
st   ───────────────────────┘└─
353    have : inf_edist x ∅ ≤ Hausdorff_edist s ∅ := inf_edist_le_Hausdorff_edist_of_mem xs,
id            └───────┘    └─────────────┘       └─────────────────────────────────┘ └┘
src    └─────┘└───────┘ └─────────────┘  └──┘└─────────────────────────────────┘
typ    └─────┘└───────┘└─────────────┘ └──┘└─────────────────────────────────┘└┘
doc    └─────┘└───────┘   └─────────────┘  └──┘└─────────────────────────────────┘
txt    └─────┘                             └──┘                                   
par    └─────┘                             └──┘                                   
pid    └───┘└┘                             └──┘                                   
st   ─────────────────────────────────────────────────────────────────────────────────────┘└─
354    simpa using this,
id                 └──┘
src    └──────────┘
typ    └──────────┘└──┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
pid         └────┘
st   ─────────────────┘└─
355  end
st   ──┘
356  
357  /-- If a set is at finite Hausdorff edistance of a nonempty set, it is nonempty -/
358  lemma nonempty_of_Hausdorff_edist_ne_top (hs : s.nonempty) (fin : Hausdorff_edist s t ≠ ⊤) :
id                                                  └───────┘         └─────────────┘    
src                                                  └───────┘         └─────────────┘      
typ                                                 └───────┘         └─────────────┘    
doc                                                  └───────┘         └─────────────┘
359    t.nonempty :=
id     └───────┘
src     └───────┘
typ    └───────┘
doc     └───────┘
360  t.eq_empty_or_nonempty.elim (λ ht, (fin $ ht.symm ▸ Hausdorff_edist_empty hs).elim) id
id   └───────────────────┘└───┘    └┘   └─┘   └┘└───┘  └───────────────────┘ └┘ └──┘   └┘
src   └───────────────────┘└───┘         └─┘     └───┘  └───────────────────┘    └──┘   └┘
typ  └───────────────────┘└───┘    └┘   └─┘   └┘└───┘  └───────────────────┘ └┘ └──┘   └┘
doc                                                      └───────────────────┘
361  
362  lemma empty_or_nonempty_of_Hausdorff_edist_ne_top (fin : Hausdorff_edist s t ≠ ⊤) :
id                                                            └─────────────┘    
src                                                           └─────────────┘      
typ                                                           └─────────────┘    
doc                                                           └─────────────┘
363    s = ∅ ∧ t = ∅ ∨ s.nonempty ∧ t.nonempty :=
id             └───────┘  └───────┘
src               └───────┘   └───────┘
typ            └───────┘  └───────┘
doc                     └───────┘    └───────┘
364  begin
st   └─────
365    cases s.eq_empty_or_nonempty with hs hs,
id           └────────────────────┘
src    └────┘└────────────────────┘└─────────┘
typ    └────┘└────────────────────┘└─────────┘
doc    └────┘                      └─────────┘
txt    └────┘                      └─────────┘
par    └────┘                      └─────────┘
pid                               └─────────┘
st   ────────────────────────────────────────┘└─
366    { cases t.eq_empty_or_nonempty with ht ht,
id             └────────────────────┘
src      └────┘└────────────────────┘└─────────┘
typ      └────┘└────────────────────┘└─────────┘
doc      └────┘                      └─────────┘
txt      └────┘                      └─────────┘
par      └────┘                      └─────────┘
pid                                 └─────────┘
st   ───┘└─────────────────────────────────────┘└─
367      { exact or.inl ⟨hs, ht⟩ },
id               └────┘  └┘  └┘
src        └────┘└────┘   └┘  └┘
typ        └────┘└────┘ └┘└┘└┘└┘
doc        └────┘         └┘  └┘
txt        └────┘         └┘  └┘
par        └────┘         └┘  └┘
pid                      └┘  
st   ─────┘└────────────────────┘└┘
368      { rw Hausdorff_edist_comm at fin,
id            └──────────────────┘
src        └─┘└──────────────────┘└─────┘
typ        └─┘└──────────────────┘└─────┘
doc        └─┘└──────────────────┘└─────┘
txt        └─┘                    └─────┘
par        └─┘                    └─────┘
pid                              └─────┘
st   ───────────────────────────────────┘└─
369        exact or.inr ⟨nonempty_of_Hausdorff_edist_ne_top ht fin, ht⟩ } },
id               └────┘  └────────────────────────────────┘    └─┘  └┘
src        └────┘└────┘ └────────────────────────────────┘  └─┘└┘  └┘
typ        └────┘└────┘ └────────────────────────────────┘  └─┘└┘└┘└┘
doc        └────┘       └────────────────────────────────┘     └┘  └┘
txt        └────┘                                              └┘  └┘
par        └────┘                                              └┘  └┘
pid                                                           └┘  
st   ──────────────────────────────────────────────────────────────────┘└──┘
370    { exact or.inr ⟨hs, nonempty_of_Hausdorff_edist_ne_top hs fin⟩ }
id             └────┘      └────────────────────────────────┘ └┘ └─┘
src      └────┘└────┘   └┘└────────────────────────────────┘  └─┘└┘
typ      └────┘└────┘   └┘└────────────────────────────────┘└┘└─┘└┘
doc      └────┘         └┘└────────────────────────────────┘     └┘
txt      └────┘         └┘                                       └┘
par      └────┘         └┘                                       └┘
pid                    └┘                                       
st   ────────────────────────────────────────────────────────────────┘└─
371  end
st   ──┘
372  
373  end Hausdorff_edist -- section
374  end emetric --namespace
375  
376  
377  /-Now, we turn to the same notions in metric spaces. To avoid the difficulties related to
378  Inf and Sup on ℝ (which is only conditionnally complete), we use the notions in ennreal formulated
379  in terms of the edistance, and coerce them to ℝ. Then their properties follow readily from the
380  corresponding properties in ennreal, modulo some tedious rewriting of inequalities from one to the
381  other -/
382  
383  namespace metric
384  section
385  variables {α : Type u} {β : Type v} [metric_space α] [metric_space β] {s t u : set α} {x y : α} {Φ : α → β}
id                                       └──────────┘     └──────────┘             └─┘
src                                       └──────────┘     └──────────┘             └─┘
typ                                      └──────────┘     └──────────┘             └─┘
doc                                       └──────────┘     └──────────┘
386  open emetric
387  
388  /-- The minimal distance of a point to a set -/
389  def inf_dist (x : α) (s : set α) : ℝ := ennreal.to_real (inf_edist x s)
id                            └─┘         └─────────────┘  └───────┘  
src                            └─┘          └─────────────┘  └───────┘
typ                           └─┘         └─────────────┘  └───────┘  
doc                                          └─────────────┘  └───────┘
390  
391  /-- the minimal distance is always nonnegative -/
392  lemma inf_dist_nonneg : 0 ≤ inf_dist x s := by simp [inf_dist]
id                              └──────┘               └──────┘
src                             └──────┘           └────┘└──────┘└─
typ                             └──────┘         └────┘└──────┘└─
doc                              └──────┘           └────┘└──────┘└─
txt                                                 └────┘        └─
par                                                 └────┘        └─
pid                                                             
st                                                 └────────────────
393  
src  
typ  
doc  
txt  
par  
pid  
st   
394  /-- the minimal distance to the empty set is 0 (if you want to have the more reasonable
395  value ∞ instead, use `inf_edist`, which takes values in ennreal) -/
396  @[simp] lemma inf_dist_empty : inf_dist x ∅ = 0 :=
id                                  └──────┘   
src                                 └──────┘    
typ                                 └──────┘   
doc    └──┘                         └──────┘
397  by simp [inf_dist]
id            └──────┘
src     └────┘└──────┘└─
typ     └────┘└──────┘└─
doc     └────┘└──────┘└─
txt     └────┘        └─
par     └────┘        └─
pid                 
st     └────────────────
398  
src  
typ  
doc  
txt  
par  
pid  
st   
399  /-- In a metric space, the minimal edistance to a nonempty set is finite -/
400  lemma inf_edist_ne_top (h : s.nonempty) : inf_edist x s ≠ ⊤ :=
id                               └───────┘    └───────┘    
src                               └───────┘    └───────┘      
typ                              └───────┘    └───────┘    
doc                               └───────┘    └───────┘
401  begin
st   └─────
402    rcases h with ⟨y, hy⟩,
id            
src    └─────┘ └───────────┘
typ    └─────┘└───────────┘
doc    └─────┘ └───────────┘
txt    └─────┘ └───────────┘
par    └─────┘ └───────────┘
pid           └───────────┘
st   ──────────────────────┘└─
403    apply lt_top_iff_ne_top.1,
id           └───────────────┘
src    └────┘└───────────────┘└┘
typ    └────┘└───────────────┘└┘
doc    └────┘                 └┘
txt    └────┘                 └┘
par    └────┘                 └┘
pid                          └┘
st   ──────────────────────────┘└─
404    calc inf_edist x s ≤ edist x y : inf_edist_le_edist_of_mem hy
id     └──┘ └───────┘      └───┘     └───────────────────────┘ └┘
src    └──┘ └───────┘       └───┘       └───────────────────────┘
typ    └──┘ └───────┘      └───┘     └───────────────────────┘ └┘
doc    └──┘ └───────┘                   └───────────────────────┘
st   ────────────────────────────────────────────────────────────────
405         ... < ⊤ : lt_top_iff_ne_top.2 (edist_ne_top _ _)
id                   └───────────────┘   └──────────┘
src                  └───────────────┘   └──────────┘
typ                  └───────────────┘   └──────────┘
doc                                        └──────────┘
st   ──────────────────────────────────────────────────────┘
406  end
st   ──┘
407  
408  /-- The minimal distance of a point to a set containing it vanishes -/
409  lemma inf_dist_zero_of_mem (h : x ∈ s) : inf_dist x s = 0 :=
id                                         └──────┘   
src                                          └──────┘     
typ                                        └──────┘   
doc                                           └──────┘
410  by simp [inf_edist_zero_of_mem h, inf_dist]
id            └───────────────────┘   └──────┘
src     └────┘└───────────────────┘ └┘└──────┘└─
typ     └────┘└───────────────────┘└┘└──────┘└─
doc     └────┘└───────────────────┘ └┘└──────┘└─
txt     └────┘                      └┘        └─
par     └────┘                      └┘        └─
pid                               └┘        
st     └─────────────────────────────────────────
411  
src  
typ  
doc  
txt  
par  
pid  
st   
412  /-- The minimal distance to a singleton is the distance to the unique point in this singleton -/
413  @[simp] lemma inf_dist_singleton : inf_dist x {y} = dist x y :=
id                                      └──────┘     └──┘  
src                                     └──────┘       └──┘
typ                                     └──────┘     └──┘  
doc    └──┘                             └──────┘
414  by simp [inf_dist, inf_edist, dist_edist]
id            └──────┘  └───────┘  └────────┘
src     └────┘└──────┘└┘└───────┘└┘└────────┘└─
typ     └────┘└──────┘└┘└───────┘└┘└────────┘└─
doc     └────┘└──────┘└┘└───────┘└┘└────────┘└─
txt     └────┘        └┘         └┘          └─
par     └────┘        └┘         └┘          └─
pid                 └┘         └┘          
st     └───────────────────────────────────────
415  
src  
typ  
doc  
txt  
par  
pid  
st   
416  /-- The minimal distance to a set is bounded by the distance to any point in this set -/
417  lemma inf_dist_le_dist_of_mem (h : y ∈ s) : inf_dist x s ≤ dist x y :=
id                                            └──────┘    └──┘  
src                                             └──────┘      └──┘
typ                                           └──────┘    └──┘  
doc                                              └──────┘
418  begin
st   └─────
419    rw [dist_edist, inf_dist, ennreal.to_real_le_to_real (inf_edist_ne_top ⟨_, h⟩) (edist_ne_top _ _)],
id         └────────┘  └──────┘  └────────────────────────┘  └──────────────┘         └──────────┘
src    └──┘└────────┘└┘└──────┘└┘└────────────────────────┘ └──────────────┘ └─┘ └─┘ └──────────┘└────┘
typ    └──┘└────────┘└┘└──────┘└┘└────────────────────────┘ └──────────────┘ └─┘└─┘ └──────────┘└────┘
doc    └──┘└────────┘└┘└──────┘└┘                           └──────────────┘ └─┘ └─┘ └──────────┘└────┘
txt    └──┘          └┘        └┘                                            └─┘ └─┘             └────┘
par    └──┘          └┘        └┘                                            └─┘ └─┘             └────┘
pid      └┘          └┘        └┘                                            └─┘ └─┘             └────┘
st   ───────────────┘└────────┘└───────────────────────────────────────────────────────────────────────┘└──
420    exact inf_edist_le_edist_of_mem h
id           └───────────────────────┘ 
src    └────┘└───────────────────────┘ 
typ    └────┘└───────────────────────┘
doc    └────┘└───────────────────────┘ 
txt    └────┘                          
par    └────┘                          
pid                                   
st   ───────────────────────────────────┘
421  end
st   └─┘
422  
423  /-- The minimal distance is monotonous with respect to inclusion -/
424  lemma inf_dist_le_inf_dist_of_subset (h : s ⊆ t) (hs : s.nonempty) :
id                                                       └───────┘
src                                                         └───────┘
typ                                                      └───────┘
doc                                                          └───────┘
425    inf_dist x t ≤ inf_dist x s :=
id     └──────┘    └──────┘  
src    └──────┘      └──────┘
typ    └──────┘    └──────┘  
doc    └──────┘       └──────┘
426  begin
st   └─────
427    have ht : t.nonempty := hs.mono h,
id               └────────┘    └─────┘ 
src    └────────┘└────────┘└──┘└─────┘
typ    └────────┘└────────┘└──┘└─────┘
doc    └────────┘└────────┘└──┘       
txt    └────────┘          └──┘       
par    └────────┘          └──┘       
pid    └─────┘└─┘          └──┘       
st   ──────────────────────────────────┘└─
428    rw [inf_dist, inf_dist, ennreal.to_real_le_to_real (inf_edist_ne_top ht) (inf_edist_ne_top hs)],
id         └──────┘  └──────┘  └────────────────────────┘                   └┘   └──────────────┘ └┘
src    └──┘└──────┘└┘└──────┘└┘└────────────────────────┘                   └┘ └──────────────┘  └┘
typ    └──┘└──────┘└┘└──────┘└┘└────────────────────────┘                 └┘└┘ └──────────────┘└┘└┘
doc    └──┘└──────┘└┘└──────┘└┘                                             └┘ └──────────────┘  └┘
txt    └──┘        └┘        └┘                                             └┘                   └┘
par    └──┘        └┘        └┘                                             └┘                   └┘
pid      └┘        └┘        └┘                                             └┘                   └┘
st   ─────────────┘└────────┘└──────────────────────────────────────────────────────────────────────┘└──
429    exact inf_edist_le_inf_edist_of_subset h
id           └──────────────────────────────┘ 
src    └────┘└──────────────────────────────┘ 
typ    └────┘└──────────────────────────────┘
doc    └────┘└──────────────────────────────┘ 
txt    └────┘                                 
par    └────┘                                 
pid                                          
st   ──────────────────────────────────────────┘
430  end
st   └─┘
431  
432  /-- If the minimal distance to a set is `<r`, there exists a point in this set at distance `<r` -/
433  lemma exists_dist_lt_of_inf_dist_lt {r : real} (h : inf_dist x s < r) (hs : s.nonempty) :
id                                            └──┘       └──────┘            └───────┘
src                                           └──┘       └──────┘                └───────┘
typ                                           └──┘       └──────┘            └───────┘
doc                                                      └──────┘                 └───────┘
434    ∃y∈s, dist x y < r :=
id       └──┘    
src        └──┘     
typ      └──┘    
435  begin
st   └─────
436    have rpos : 0 < r := lt_of_le_of_lt inf_dist_nonneg h,
id                        └────────────┘ └─────────────┘ 
src    └────────────┘ └──┘└────────────┘└─────────────┘
typ    └────────────┘└──┘└────────────┘└─────────────┘
doc    └────────────┘  └──┘              └─────────────┘
txt    └────────────┘  └──┘                             
par    └────────────┘  └──┘                             
pid    └───────┘└───┘  └──┘                             
st   ──────────────────────────────────────────────────────┘└─
437    have : inf_edist x s < ennreal.of_real r,
id            └───────┘     └─────────────┘ 
src    └─────┘└───────┘   └─────────────┘
typ    └─────┘└───────┘ └─────────────┘
doc    └─────┘└───────┘   └─────────────┘
txt    └─────┘                           
par    └─────┘                           
pid    └───┘└┘                           
st   ─────────────────────────────────────────┘└─
438    { rwa [inf_dist, ← ennreal.to_real_of_real (le_of_lt rpos), ennreal.to_real_lt_to_real (inf_edist_ne_top hs)] at h,
id            └──────┘    └─────────────────────┘  └──────┘ └──┘   └────────────────────────┘  └──────────────┘ └┘
src      └───┘└──────┘└──┘└─────────────────────┘ └──────┘    └─┘└────────────────────────┘ └──────────────┘  └─────┘
typ      └───┘└──────┘└──┘└─────────────────────┘ └──────┘└──┘└─┘└────────────────────────┘ └──────────────┘└┘└─────┘
doc      └───┘└──────┘└──┘                                    └─┘                           └──────────────┘  └─────┘
txt      └───┘        └──┘                                    └─┘                                             └─────┘
par      └───┘        └──┘                                    └─┘                                             └─────┘
pid         └┘        └──┘                                    └─┘                                             └┘└───┘
st   ───┘└───────────┘└─────────────────────────────────────────┘└────────────────────────────────────────────────┘└───┘└─
439      simp },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ────────┘└┘
440    rcases exists_edist_lt_of_inf_edist_lt this with ⟨y, ys, hy⟩,
id            └─────────────────────────────┘ └──┘
src    └─────┘└─────────────────────────────┘    └───────────────┘
typ    └─────┘└─────────────────────────────┘└──┘└───────────────┘
doc    └─────┘└─────────────────────────────┘    └───────────────┘
txt    └─────┘                                   └───────────────┘
par    └─────┘                                   └───────────────┘
pid                                             └───────────────┘
st   ─────────────────────────────────────────────────────────────┘└─
441    rw [edist_dist, ennreal.of_real_lt_of_real_iff rpos] at hy,
id         └────────┘  └────────────────────────────┘ └──┘
src    └──┘└────────┘└┘└────────────────────────────┘    └─────┘
typ    └──┘└────────┘└┘└────────────────────────────┘└──┘└─────┘
doc    └──┘          └┘                                  └─────┘
txt    └──┘          └┘                                  └─────┘
par    └──┘          └┘                                  └─────┘
pid      └┘          └┘                                  └────┘
st   ───────────────┘└───────────────────────────────────┘└────┘└─
442    exact ⟨y, ys, hy⟩,
id              └┘  └┘
src    └────┘  └┘  └┘  
typ    └────┘ └┘└┘└┘└┘
doc    └────┘  └┘  └┘  
txt    └────┘  └┘  └┘  
par    └────┘  └┘  └┘  
pid           └┘  └┘  
st   ──────────────────┘└─
443  end
st   ──┘
444  
445  /-- The minimal distance from `x` to `s` is bounded by the distance from `y` to `s`, modulo
446  the distance between `x` and `y` -/
447  lemma inf_dist_le_inf_dist_add_dist : inf_dist x s ≤ inf_dist y s + dist x y :=
id                                         └──────┘    └──────┘    └──┘  
src                                        └──────┘      └──────┘      └──┘
typ                                        └──────┘    └──────┘    └──┘  
doc                                        └──────┘       └──────┘
448  begin
st   └─────
449    cases s.eq_empty_or_nonempty with hs hs,
id           └────────────────────┘
src    └────┘└────────────────────┘└─────────┘
typ    └────┘└────────────────────┘└─────────┘
doc    └────┘                      └─────────┘
txt    └────┘                      └─────────┘
par    └────┘                      └─────────┘
pid                               └─────────┘
st   ────────────────────────────────────────┘└─
450    { by simp [hs, dist_nonneg] },
id                └┘  └─────────┘
src         └────┘  └┘└─────────┘└┘
typ         └────┘└┘└┘└─────────┘└┘
doc         └────┘  └┘           └┘
txt         └────┘  └┘           └┘
par         └────┘  └┘           └┘
pid               └┘           
st   ───┘                          └┘
451    { rw [inf_dist, inf_dist, dist_edist, ← ennreal.to_real_add (inf_edist_ne_top hs) (edist_ne_top _ _),
id           └──────┘  └──────┘  └────────┘    └─────────────────┘  └──────────────┘ └┘   └──────────┘
src      └──┘└──────┘└┘└──────┘└┘└────────┘└──┘└─────────────────┘ └──────────────┘  └┘ └──────────┘└──────
typ      └──┘└──────┘└┘└──────┘└┘└────────┘└──┘└─────────────────┘ └──────────────┘└┘└┘ └──────────┘└──────
doc      └──┘└──────┘└┘└──────┘└┘└────────┘└──┘                    └──────────────┘  └┘ └──────────┘└──────
txt      └──┘        └┘        └┘          └──┘                                      └┘             └──────
par      └──┘        └┘        └┘          └──┘                                      └┘             └──────
pid        └┘        └┘        └┘          └──┘                                      └┘             └──────
st   ───────────────┘└────────┘└──────────┘└──────────────────────────────────────────────────────────────┘└─
452          ennreal.to_real_le_to_real (inf_edist_ne_top hs)],
id           └────────────────────────┘  └──────────────┘ └┘
src  ───────┘└────────────────────────┘ └──────────────┘  └┘
typ  ───────┘└────────────────────────┘ └──────────────┘└┘└┘
doc  ───────┘                           └──────────────┘  └┘
txt  ───────┘                                             └┘
par  ───────┘                                             └┘
pid  ───────┘                                             └┘
st   ───────────────────────────────────────────────────────┘└─
453      { apply inf_edist_le_inf_edist_add_edist },
id               └──────────────────────────────┘
src        └────┘└──────────────────────────────┘
typ        └────┘└──────────────────────────────┘
doc        └────┘└──────────────────────────────┘
txt        └────┘                                
par        └────┘                                
pid                                             
st   ─────┘└─────────────────────────────────────┘└┘
454      { simp [ennreal.add_eq_top, inf_edist_ne_top hs, edist_ne_top] }}
id               └────────────────┘  └──────────────┘ └┘  └──────────┘
src        └────┘└────────────────┘└┘└──────────────┘  └┘└──────────┘└┘
typ        └────┘└────────────────┘└┘└──────────────┘└┘└┘└──────────┘└┘
doc        └────┘                  └┘└──────────────┘  └┘└──────────┘└┘
txt        └────┘                  └┘                  └┘            └┘
par        └────┘                  └┘                  └┘            └┘
pid                              └┘                  └┘            
st   ──────────────────────────────────────────────────────────────────┘└──
455  end
st   ──┘
456  
457  variable (s)
458  
459  /-- The minimal distance to a set is Lipschitz in point with constant 1 -/
460  lemma lipschitz_inf_dist_pt : lipschitz_with 1 (λx, inf_dist x s) :=
id                                 └────────────┘       └──────┘  
src                                └────────────┘        └──────┘
typ                                └────────────┘       └──────┘  
doc                                └────────────┘        └──────┘
461  lipschitz_with.one_of_le_add $ λ x y, inf_dist_le_inf_dist_add_dist
id   └──────────────────────────┘        └───────────────────────────┘
src  └──────────────────────────┘          └───────────────────────────┘
typ  └──────────────────────────┘        └───────────────────────────┘
doc                                        └───────────────────────────┘
462  
463  /-- The minimal distance to a set is uniformly continuous in point -/
464  lemma uniform_continuous_inf_dist_pt :
465    uniform_continuous (λx, inf_dist x s) :=
id     └────────────────┘     └──────┘  
src    └────────────────┘      └──────┘
typ    └────────────────┘     └──────┘  
doc                            └──────┘
466  (lipschitz_inf_dist_pt s).to_uniform_continuous
id    └───────────────────┘  └───────────────────┘
src   └───────────────────┘   └───────────────────┘
typ   └───────────────────┘  └───────────────────┘
doc   └───────────────────┘   └───────────────────┘
467  
468  /-- The minimal distance to a set is continuous in point -/
469  lemma continuous_inf_dist_pt : continuous (λx, inf_dist x s) :=
id                                  └────────┘     └──────┘  
src                                 └────────┘      └──────┘
typ                                 └────────┘     └──────┘  
doc                                 └────────┘      └──────┘
470  (uniform_continuous_inf_dist_pt s).continuous
id    └────────────────────────────┘  └────────┘
src   └────────────────────────────┘   └────────┘
typ   └────────────────────────────┘  └────────┘
doc   └────────────────────────────┘
471  
472  variable {s}
473  
474  /-- The minimal distance to a set and its closure coincide -/
475  lemma inf_dist_eq_closure : inf_dist x (closure s) = inf_dist x s :=
id                               └──────┘   └─────┘    └──────┘  
src                              └──────┘    └─────┘     └──────┘
typ                              └──────┘   └─────┘    └──────┘  
doc                              └──────┘    └─────┘      └──────┘
476  by simp [inf_dist, inf_edist_closure]
id            └──────┘  └───────────────┘
src     └────┘└──────┘└┘└───────────────┘└─
typ     └────┘└──────┘└┘└───────────────┘└─
doc     └────┘└──────┘└┘└───────────────┘└─
txt     └────┘        └┘                 └─
par     └────┘        └┘                 └─
pid                 └┘                 
st     └───────────────────────────────────
477  
src  
typ  
doc  
txt  
par  
pid  
st   
478  /-- A point belongs to the closure of `s` iff its infimum distance to this set vanishes -/
479  lemma mem_closure_iff_inf_dist_zero (h : s.nonempty) : x ∈ closure s ↔ inf_dist x s = 0 :=
id                                            └───────┘      └─────┘   └──────┘   
src                                            └───────┘       └─────┘    └──────┘     
typ                                           └───────┘      └─────┘   └──────┘   
doc                                            └───────┘        └─────┘     └──────┘
480  by simp [mem_closure_iff_inf_edist_zero, inf_dist, ennreal.to_real_eq_zero_iff, inf_edist_ne_top h]
id            └────────────────────────────┘  └──────┘  └─────────────────────────┘  └──────────────┘ 
src     └────┘└────────────────────────────┘└┘└──────┘└┘└─────────────────────────┘└┘└──────────────┘ └─
typ     └────┘└────────────────────────────┘└┘└──────┘└┘└─────────────────────────┘└┘└──────────────┘└─
doc     └────┘└────────────────────────────┘└┘└──────┘└┘                           └┘└──────────────┘ └─
txt     └────┘                              └┘        └┘                           └┘                 └─
par     └────┘                              └┘        └┘                           └┘                 └─
pid                                       └┘        └┘                           └┘                 
st     └─────────────────────────────────────────────────────────────────────────────────────────────────
481  
src  
typ  
doc  
txt  
par  
pid  
st   
482  /-- Given a closed set `s`, a point belongs to `s` iff its infimum distance to this set vanishes -/
483  lemma mem_iff_inf_dist_zero_of_closed (h : is_closed s) (hs : s.nonempty) :
id                                              └───────┘         └───────┘
src                                             └───────┘           └───────┘
typ                                             └───────┘         └───────┘
doc                                             └───────┘           └───────┘
484    x ∈ s ↔ inf_dist x s = 0 :=
id         └──────┘   
src          └──────┘     
typ        └──────┘   
doc            └──────┘
485  begin
st   └─────
486    have := @mem_closure_iff_inf_dist_zero _ _ s x hs,
id              └───────────────────────────┘       └┘
src    └──────┘ └───────────────────────────┘└───┘  
typ    └──────┘ └───────────────────────────┘└───┘└┘
doc    └──────┘ └───────────────────────────┘└───┘  
txt    └──────┘                              └───┘  
par    └──────┘                              └───┘  
pid    └───┘└─┘                              └───┘  
st   ──────────────────────────────────────────────────┘└─
487    rwa closure_eq_iff_is_closed.2 h at this
id         └──────────────────────┘   
src    └──┘└──────────────────────┘└─┘ └───────┘
typ    └──┘└──────────────────────┘└─┘└───────┘
doc    └──┘                        └─┘ └───────┘
txt    └──┘                        └─┘ └───────┘
par    └──┘                        └─┘ └───────┘
pid                               └─┘ └──────┘
st   ──────────────────────────────────────────┘
488  end
st   └─┘
489  
490  /-- The infimum distance is invariant under isometries -/
491  lemma inf_dist_image (hΦ : isometry Φ) :
id                              └──────┘ 
src                             └──────┘
typ                             └──────┘ 
doc                             └──────┘
492    inf_dist (Φ x) (Φ '' t) = inf_dist x t :=
id     └──────┘       └┘    └──────┘  
src    └──────┘          └┘     └──────┘
typ    └──────┘       └┘    └──────┘  
doc    └──────┘                  └──────┘
493  by simp [inf_dist, inf_edist_image hΦ]
id            └──────┘  └─────────────┘ └┘
src     └────┘└──────┘└┘└─────────────┘  └─
typ     └────┘└──────┘└┘└─────────────┘└┘└─
doc     └────┘└──────┘└┘└─────────────┘  └─
txt     └────┘        └┘                 └─
par     └────┘        └┘                 └─
pid                 └┘                 
st     └────────────────────────────────────
494  
src  
typ  
doc  
txt  
par  
pid  
st   
495  /-- The Hausdorff distance between two sets is the smallest nonnegative `r` such that each set is
496  included in the `r`-neighborhood of the other. If there is no such `r`, it is defined to
497  be `0`, arbitrarily -/
498  def Hausdorff_dist (s t : set α) : ℝ := ennreal.to_real (Hausdorff_edist s t)
id                             └─┘         └─────────────┘  └─────────────┘  
src                            └─┘          └─────────────┘  └─────────────┘
typ                            └─┘         └─────────────┘  └─────────────┘  
doc                                          └─────────────┘  └─────────────┘
499  
500  /-- The Hausdorff distance is nonnegative -/
501  lemma Hausdorff_dist_nonneg : 0 ≤ Hausdorff_dist s t :=
id                                    └────────────┘  
src                                   └────────────┘
typ                                   └────────────┘  
doc                                    └────────────┘
502  by simp [Hausdorff_dist]
id            └────────────┘
src     └────┘└────────────┘└─
typ     └────┘└────────────┘└─
doc     └────┘└────────────┘└─
txt     └────┘              └─
par     └────┘              └─
pid                       
st     └──────────────────────
503  
src  
typ  
doc  
txt  
par  
pid  
st   
504  /-- If two sets are nonempty and bounded in a metric space, they are at finite Hausdorff edistance -/
505  lemma Hausdorff_edist_ne_top_of_nonempty_of_bounded (hs : s.nonempty) (ht : t.nonempty)
id                                                             └───────┘        └───────┘
src                                                             └───────┘         └───────┘
typ                                                            └───────┘        └───────┘
doc                                                             └───────┘         └───────┘
506    (bs : bounded s) (bt : bounded t) : Hausdorff_edist s t ≠ ⊤ :=
id           └─────┘         └─────┘     └─────────────┘    
src          └─────┘          └─────┘      └─────────────┘      
typ          └─────┘         └─────┘     └─────────────┘    
doc          └─────┘          └─────┘      └─────────────┘
507  begin
st   └─────
508    rcases hs with ⟨cs, hcs⟩,
id            └┘
src    └─────┘  └─────────────┘
typ    └─────┘└┘└─────────────┘
doc    └─────┘  └─────────────┘
txt    └─────┘  └─────────────┘
par    └─────┘  └─────────────┘
pid            └─────────────┘
st   ─────────────────────────┘└─
509    rcases ht with ⟨ct, hct⟩,
id            └┘
src    └─────┘  └─────────────┘
typ    └─────┘└┘└─────────────┘
doc    └─────┘  └─────────────┘
txt    └─────┘  └─────────────┘
par    └─────┘  └─────────────┘
pid            └─────────────┘
st   ─────────────────────────┘└─
510    rcases (bounded_iff_subset_ball ct).1 bs with ⟨rs, hrs⟩,
id             └─────────────────────┘ └┘    └┘
src    └─────┘ └─────────────────────┘  └──┘  └─────────────┘
typ    └─────┘ └─────────────────────┘└┘└──┘└┘└─────────────┘
doc    └─────┘ └─────────────────────┘  └──┘  └─────────────┘
txt    └─────┘                          └──┘  └─────────────┘
par    └─────┘                          └──┘  └─────────────┘
pid                                    └──┘  └─────────────┘
st   ────────────────────────────────────────────────────────┘└─
511    rcases (bounded_iff_subset_ball cs).1 bt with ⟨rt, hrt⟩,
id             └─────────────────────┘ └┘    └┘
src    └─────┘ └─────────────────────┘  └──┘  └─────────────┘
typ    └─────┘ └─────────────────────┘└┘└──┘└┘└─────────────┘
doc    └─────┘ └─────────────────────┘  └──┘  └─────────────┘
txt    └─────┘                          └──┘  └─────────────┘
par    └─────┘                          └──┘  └─────────────┘
pid                                    └──┘  └─────────────┘
st   ────────────────────────────────────────────────────────┘└─
512    have : Hausdorff_edist s t ≤ ennreal.of_real (max rs rt),
id            └─────────────┘    └─────────────┘  └─┘ └┘ └┘
src    └─────┘└─────────────┘  └─────────────┘ └─┘    
typ    └─────┘└─────────────┘└─────────────┘ └─┘└┘└┘
doc    └─────┘└─────────────┘   └─────────────┘        
txt    └─────┘                                         
par    └─────┘                                         
pid    └───┘└┘                                         
st   ─────────────────────────────────────────────────────────┘└─
513    { apply Hausdorff_edist_le_of_mem_edist,
id             └─────────────────────────────┘
src      └────┘└─────────────────────────────┘
typ      └────┘└─────────────────────────────┘
doc      └────┘└─────────────────────────────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└───────────────────────────────────┘└─
514      { assume x xs,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid        └─────────┘
st   ─────┘└─────────┘└─
515        existsi [ct, hct],
id                  └┘  └─┘
src        └───────┘  └┘   
typ        └───────┘└┘└┘└─┘
doc        └───────┘  └┘   
txt        └───────┘  └┘   
par        └───────┘  └┘   
pid               └┘  └┘   
st   ──────────────────────┘└─
516        have : dist x ct ≤ max rs rt := le_trans (hrs xs) (le_max_left _ _),
id                └──┘  └┘   └─┘ └┘ └┘    └──────┘  └─┘ └┘   └─────────┘
src        └─────┘└──┘    └─┘    └──┘└──────┘      └┘ └─────────┘└───┘
typ        └─────┘└──┘└┘ └─┘└┘└┘└──┘└──────┘ └─┘└┘└┘ └─────────┘└───┘
doc        └─────┘               └──┘              └┘            └───┘
txt        └─────┘               └──┘              └┘            └───┘
par        └─────┘               └──┘              └┘            └───┘
pid        └───┘└┘               └──┘              └┘            └───┘
st   ────────────────────────────────────────────────────────────────────────┘└─
517        rwa [edist_dist, ennreal.of_real_le_of_real_iff],
id              └────────┘  └────────────────────────────┘
src        └───┘└────────┘└┘└────────────────────────────┘
typ        └───┘└────────┘└┘└────────────────────────────┘
doc        └───┘          └┘                              
txt        └───┘          └┘                              
par        └───┘          └┘                              
pid           └┘          └┘                              
st   ────────────────────┘└──────────────────────────────┘└─
518        exact le_trans dist_nonneg this },
id               └──────┘ └─────────┘ └──┘
src        └────┘└──────┘└─────────┘    
typ        └────┘└──────┘└─────────┘└──┘
doc        └────┘                       
txt        └────┘                       
par        └────┘                       
pid                                    
st   ─────────────────────────────────────┘└┘
519      { assume x xt,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid        └─────────┘
st   ────────────────┘└─
520        existsi [cs, hcs],
id                  └┘  └─┘
src        └───────┘  └┘   
typ        └───────┘└┘└┘└─┘
doc        └───────┘  └┘   
txt        └───────┘  └┘   
par        └───────┘  └┘   
pid               └┘  └┘   
st   ──────────────────────┘└─
521        have : dist x cs ≤ max rs rt := le_trans (hrt xt) (le_max_right _ _),
id                └──┘  └┘   └─┘ └┘ └┘    └──────┘  └─┘ └┘   └──────────┘
src        └─────┘└──┘    └─┘    └──┘└──────┘      └┘ └──────────┘└───┘
typ        └─────┘└──┘└┘ └─┘└┘└┘└──┘└──────┘ └─┘└┘└┘ └──────────┘└───┘
doc        └─────┘               └──┘              └┘             └───┘
txt        └─────┘               └──┘              └┘             └───┘
par        └─────┘               └──┘              └┘             └───┘
pid        └───┘└┘               └──┘              └┘             └───┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
522        rwa [edist_dist, ennreal.of_real_le_of_real_iff],
id              └────────┘  └────────────────────────────┘
src        └───┘└────────┘└┘└────────────────────────────┘
typ        └───┘└────────┘└┘└────────────────────────────┘
doc        └───┘          └┘                              
txt        └───┘          └┘                              
par        └───┘          └┘                              
pid           └┘          └┘                              
st   ────────────────────┘└──────────────────────────────┘└─
523        exact le_trans dist_nonneg this }},
id               └──────┘ └─────────┘ └──┘
src        └────┘└──────┘└─────────┘    
typ        └────┘└──────┘└─────────┘└──┘
doc        └────┘                       
txt        └────┘                       
par        └────┘                       
pid                                    
st   ─────────────────────────────────────┘└─┘
524    exact ennreal.lt_top_iff_ne_top.1 (lt_of_le_of_lt this (by simp [lt_top_iff_ne_top]))
id           └───────────────────────┘    └────────────┘ └──┘           └───────────────┘
src    └────┘└───────────────────────┘└─┘ └────────────┘       └────┘└───────────────┘└─┘
typ    └────┘└───────────────────────┘└─┘ └────────────┘└──┘   └────┘└───────────────┘└─┘
doc    └────┘                         └─┘                      └────┘                 └─┘
txt    └────┘                         └─┘                      └────┘                 └─┘
par    └────┘                         └─┘                      └────┘                 └─┘
pid                                  └─┘                      └─────┘                 └─┘
st   ───────────────────────────────────────────────────────────┘└───────────────────────┘└─┘
525  end
st   └─┘
526  
527  /-- The Hausdorff distance between a set and itself is zero -/
528  @[simp] lemma Hausdorff_dist_self_zero : Hausdorff_dist s s = 0 :=
id                                            └────────────┘   
src                                           └────────────┘     
typ                                           └────────────┘   
doc    └──┘                                   └────────────┘
529  by simp [Hausdorff_dist]
id            └────────────┘
src     └────┘└────────────┘└─
typ     └────┘└────────────┘└─
doc     └────┘└────────────┘└─
txt     └────┘              └─
par     └────┘              └─
pid                       
st     └──────────────────────
530  
src  
typ  
doc  
txt  
par  
pid  
st   
531  /-- The Hausdorff distance from `s` to `t` and from `t` to `s` coincide -/
532  lemma Hausdorff_dist_comm : Hausdorff_dist s t = Hausdorff_dist t s :=
id                               └────────────┘    └────────────┘  
src                              └────────────┘      └────────────┘
typ                              └────────────┘    └────────────┘  
doc                              └────────────┘       └────────────┘
533  by simp [Hausdorff_dist, Hausdorff_edist_comm]
id            └────────────┘  └──────────────────┘
src     └────┘└────────────┘└┘└──────────────────┘└─
typ     └────┘└────────────┘└┘└──────────────────┘└─
doc     └────┘└────────────┘└┘└──────────────────┘└─
txt     └────┘              └┘                    └─
par     └────┘              └┘                    └─
pid                       └┘                    
st     └────────────────────────────────────────────
534  
src  
typ  
doc  
txt  
par  
pid  
st   
535  /-- The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable
536  value ∞ instead, use `Hausdorff_edist`, which takes values in ennreal) -/
537  @[simp] lemma Hausdorff_dist_empty : Hausdorff_dist s ∅ = 0 :=
id                                        └────────────┘   
src                                       └────────────┘    
typ                                       └────────────┘   
doc    └──┘                               └────────────┘
538  begin
st   └─────
539    cases s.eq_empty_or_nonempty with h h,
id           └────────────────────┘
src    └────┘└────────────────────┘└───────┘
typ    └────┘└────────────────────┘└───────┘
doc    └────┘                      └───────┘
txt    └────┘                      └───────┘
par    └────┘                      └───────┘
pid                               └───────┘
st   ──────────────────────────────────────┘└─
540    { simp [h] },
id             
src      └────┘ └┘
typ      └────┘└┘
doc      └────┘ └┘
txt      └────┘ └┘
par      └────┘ └┘
pid           
st   ───┘└───────┘└┘
541    { simp [Hausdorff_dist, Hausdorff_edist_empty h] }
id             └────────────┘  └───────────────────┘ 
src      └────┘└────────────┘└┘└───────────────────┘ └┘
typ      └────┘└────────────┘└┘└───────────────────┘└┘
doc      └────┘└────────────┘└┘└───────────────────┘ └┘
txt      └────┘              └┘                      └┘
par      └────┘              └┘                      └┘
pid                        └┘                      
st   ──────────────────────────────────────────────────┘└─
542  end
st   ──┘
543  
544  /-- The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable
545  value ∞ instead, use `Hausdorff_edist`, which takes values in ennreal) -/
546  @[simp] lemma Hausdorff_dist_empty' : Hausdorff_dist ∅ s = 0 :=
id                                         └────────────┘   
src                                        └────────────┘    
typ                                        └────────────┘   
doc    └──┘                                └────────────┘
547  by simp [Hausdorff_dist_comm]
id            └─────────────────┘
src     └────┘└─────────────────┘└─
typ     └────┘└─────────────────┘└─
doc     └────┘└─────────────────┘└─
txt     └────┘                   └─
par     └────┘                   └─
pid                            
st     └───────────────────────────
548  
src  
typ  
doc  
txt  
par  
pid  
st   
549  /-- Bounding the Hausdorff distance by bounding the distance of any point
550  in each set to the other set -/
551  lemma Hausdorff_dist_le_of_inf_dist {r : ℝ} (hr : r ≥ 0)
id                                                     
src                                                     
typ                                                    
552    (H1 : ∀x ∈ s, inf_dist x t ≤ r) (H2 : ∀x ∈ t, inf_dist x s ≤ r) :
id                 └──────┘                  └──────┘    
src                  └──────┘                       └──────┘     
typ                └──────┘                  └──────┘    
doc                  └──────┘                        └──────┘
553    Hausdorff_dist s t ≤ r :=
id     └────────────┘    
src    └────────────┘     
typ    └────────────┘    
doc    └────────────┘
554  begin
st   └─────
555    by_cases h1 : Hausdorff_edist s t = ⊤,
id                   └─────────────┘    
src    └───────┘  └─┘└─────────────┘  
typ    └───────┘  └─┘└─────────────┘
doc    └───────┘  └─┘└─────────────┘   
txt    └───────┘  └─┘                  
par    └───────┘  └─┘                  
pid              └─┘                  
st   ──────────────────────────────────────┘
556      by rwa [Hausdorff_dist, h1, ennreal.top_to_real],
id               └────────────┘  └┘  └─────────────────┘
src         └───┘└────────────┘└┘  └┘└─────────────────┘
typ         └───┘└────────────┘└┘└┘└┘└─────────────────┘
doc         └───┘└────────────┘└┘  └┘                   
txt         └───┘              └┘  └┘                   
par         └───┘              └┘  └┘                   
pid            └┘              └┘  └┘                   
st               └────────────┘└──┘└───────────────────┘└─
557    cases s.eq_empty_or_nonempty with hs hs,
id           └────────────────────┘
src    └────┘└────────────────────┘└─────────┘
typ    └────┘└────────────────────┘└─────────┘
doc    └────┘                      └─────────┘
txt    └────┘                      └─────────┘
par    └────┘                      └─────────┘
pid                               └─────────┘
st   ────────────────────────────────────────┘
558      by rwa [hs, Hausdorff_dist_empty'],
id               └┘  └───────────────────┘
src         └───┘  └┘└───────────────────┘
typ         └───┘└┘└┘└───────────────────┘
doc         └───┘  └┘└───────────────────┘
txt         └───┘  └┘                     
par         └───┘  └┘                     
pid            └┘  └┘                     
st               └┘└─────────────────────┘└─
559    cases t.eq_empty_or_nonempty with ht ht,
id           └────────────────────┘
src    └────┘└────────────────────┘└─────────┘
typ    └────┘└────────────────────┘└─────────┘
doc    └────┘                      └─────────┘
txt    └────┘                      └─────────┘
par    └────┘                      └─────────┘
pid                               └─────────┘
st   ────────────────────────────────────────┘
560      by rwa [ht, Hausdorff_dist_empty],
id               └┘  └──────────────────┘
src         └───┘  └┘└──────────────────┘
typ         └───┘└┘└┘└──────────────────┘
doc         └───┘  └┘└──────────────────┘
txt         └───┘  └┘                    
par         └───┘  └┘                    
pid            └┘  └┘                    
st               └┘└────────────────────┘└─
561    have : Hausdorff_edist s t ≤ ennreal.of_real r,
id            └─────────────┘    └─────────────┘ 
src    └─────┘└─────────────┘  └─────────────┘
typ    └─────┘└─────────────┘└─────────────┘
doc    └─────┘└─────────────┘   └─────────────┘
txt    └─────┘                                 
par    └─────┘                                 
pid    └───┘└┘                                 
st   ───────────────────────────────────────────────┘└─
562    { apply Hausdorff_edist_le_of_inf_edist _ _,
id             └─────────────────────────────┘
src      └────┘└─────────────────────────────┘└──┘
typ      └────┘└─────────────────────────────┘└──┘
doc      └────┘└─────────────────────────────┘└──┘
txt      └────┘                               └──┘
par      └────┘                               └──┘
pid                                          └──┘
st   ───┘└───────────────────────────────────────┘└─
563      { assume x hx,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid        └─────────┘
st   ─────┘└─────────┘└─
564        have I := H1 x hx,
id                   └┘  └┘
src        └────────┘   
typ        └────────┘└┘└┘
doc        └────────┘   
txt        └────────┘   
par        └────────┘   
pid        └────┘└─┘   
st   ──────────────────────┘└─
565        rwa [inf_dist, ← ennreal.to_real_of_real hr,
id              └──────┘    └─────────────────────┘ └┘
src        └───┘└──────┘└──┘└─────────────────────┘  └─
typ        └───┘└──────┘└──┘└─────────────────────┘└┘└─
doc        └───┘└──────┘└──┘                         └─
txt        └───┘        └──┘                         └─
par        └───┘        └──┘                         └─
pid           └┘        └──┘                         └─
st   ──────────────────┘└────────────────────────────┘└─
566             ennreal.to_real_le_to_real (inf_edist_ne_top ht) ennreal.of_real_ne_top] at I },
id              └────────────────────────┘  └──────────────┘ └┘  └────────────────────┘
src  ──────────┘└────────────────────────┘ └──────────────┘  └┘└────────────────────┘└─────┘
typ  ──────────┘└────────────────────────┘ └──────────────┘└┘└┘└────────────────────┘└─────┘
doc  ──────────┘                           └──────────────┘  └┘                      └─────┘
txt  ──────────┘                                             └┘                      └─────┘
par  ──────────┘                                             └┘                      └─────┘
pid  ──────────┘                                             └┘                      └───┘
st   ─────────────────────────────────────────────────────────────────────────────────┘└────┘└┘
567      { assume x hx,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid        └─────────┘
st   ────────────────┘└─
568        have I := H2 x hx,
id                   └┘  └┘
src        └────────┘   
typ        └────────┘└┘└┘
doc        └────────┘   
txt        └────────┘   
par        └────────┘   
pid        └────┘└─┘   
st   ──────────────────────┘└─
569        rwa [inf_dist, ← ennreal.to_real_of_real hr,
id              └──────┘    └─────────────────────┘ └┘
src        └───┘└──────┘└──┘└─────────────────────┘  └─
typ        └───┘└──────┘└──┘└─────────────────────┘└┘└─
doc        └───┘└──────┘└──┘                         └─
txt        └───┘        └──┘                         └─
par        └───┘        └──┘                         └─
pid           └┘        └──┘                         └─
st   ──────────────────┘└────────────────────────────┘└─
570             ennreal.to_real_le_to_real (inf_edist_ne_top hs) ennreal.of_real_ne_top] at I }},
id              └────────────────────────┘  └──────────────┘ └┘  └────────────────────┘
src  ──────────┘└────────────────────────┘ └──────────────┘  └┘└────────────────────┘└─────┘
typ  ──────────┘└────────────────────────┘ └──────────────┘└┘└┘└────────────────────┘└─────┘
doc  ──────────┘                           └──────────────┘  └┘                      └─────┘
txt  ──────────┘                                             └┘                      └─────┘
par  ──────────┘                                             └┘                      └─────┘
pid  ──────────┘                                             └┘                      └───┘
st   ─────────────────────────────────────────────────────────────────────────────────┘└────┘└─┘
571    rwa [Hausdorff_dist, ← ennreal.to_real_of_real hr,
id          └────────────┘    └─────────────────────┘ └┘
src    └───┘└────────────┘└──┘└─────────────────────┘  └─
typ    └───┘└────────────┘└──┘└─────────────────────┘└┘└─
doc    └───┘└────────────┘└──┘                         └─
txt    └───┘              └──┘                         └─
par    └───┘              └──┘                         └─
pid       └┘              └──┘                         └─
st   ────────────────────┘└────────────────────────────┘└─
572         ennreal.to_real_le_to_real h1 ennreal.of_real_ne_top]
id          └────────────────────────┘ └┘ └────────────────────┘
src  ──────┘└────────────────────────┘  └────────────────────┘└┘
typ  ──────┘└────────────────────────┘└┘└────────────────────┘└┘
doc  ──────┘                                                  └┘
txt  ──────┘                                                  └┘
par  ──────┘                                                  └┘
pid  ──────┘                                                  
st   ──────────────────────────────────────────────────────────┘
573  end
st   └─┘
574  
575  /-- Bounding the Hausdorff distance by exhibiting, for any point in each set,
576  another point in the other set at controlled distance -/
577  lemma Hausdorff_dist_le_of_mem_dist {r : ℝ} (hr : 0 ≤ r)
id                                                       
src                                                     
typ                                                      
578    (H1 : ∀x ∈ s, ∃y ∈ t, dist x y ≤ r) (H2 : ∀x ∈ t, ∃y ∈ s, dist x y ≤ r) :
id                     └──┘                      └──┘    
src                        └──┘                             └──┘     
typ                    └──┘                      └──┘    
579    Hausdorff_dist s t ≤ r :=
id     └────────────┘    
src    └────────────┘     
typ    └────────────┘    
doc    └────────────┘
580  begin
st   └─────
581    apply Hausdorff_dist_le_of_inf_dist hr,
id           └───────────────────────────┘ └┘
src    └────┘└───────────────────────────┘
typ    └────┘└───────────────────────────┘└┘
doc    └────┘└───────────────────────────┘
txt    └────┘                             
par    └────┘                             
pid                                      
st   ───────────────────────────────────────┘└─
582    { assume x xs,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
583      rcases H1 x xs with ⟨y, yt, hy⟩,
id              └┘  └┘
src      └─────┘     └───────────────┘
typ      └─────┘└┘└┘└───────────────┘
doc      └─────┘     └───────────────┘
txt      └─────┘     └───────────────┘
par      └─────┘     └───────────────┘
pid                 └───────────────┘
st   ──────────────────────────────────┘└─
584      exact le_trans (inf_dist_le_dist_of_mem yt) hy },
id             └──────┘  └─────────────────────┘ └┘  └┘
src      └────┘└──────┘ └─────────────────────┘  └┘  
typ      └────┘└──────┘ └─────────────────────┘└┘└┘└┘
doc      └────┘         └─────────────────────┘  └┘  
txt      └────┘                                  └┘  
par      └────┘                                  └┘  
pid                                             └┘  
st   ──────────────────────────────────────────────────┘└┘
585    { assume x xt,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ──────────────┘└─
586      rcases H2 x xt with ⟨y, ys, hy⟩,
id              └┘  └┘
src      └─────┘     └───────────────┘
typ      └─────┘└┘└┘└───────────────┘
doc      └─────┘     └───────────────┘
txt      └─────┘     └───────────────┘
par      └─────┘     └───────────────┘
pid                 └───────────────┘
st   ──────────────────────────────────┘└─
587      exact le_trans (inf_dist_le_dist_of_mem ys) hy }
id             └──────┘  └─────────────────────┘ └┘  └┘
src      └────┘└──────┘ └─────────────────────┘  └┘  
typ      └────┘└──────┘ └─────────────────────┘└┘└┘└┘
doc      └────┘         └─────────────────────┘  └┘  
txt      └────┘                                  └┘  
par      └────┘                                  └┘  
pid                                             └┘  
st   ──────────────────────────────────────────────────┘└─
588  end
st   ──┘
589  
590  /-- The Hausdorff distance is controlled by the diameter of the union -/
591  lemma Hausdorff_dist_le_diam (hs : s.nonempty) (bs : bounded s) (ht : t.nonempty) (bt : bounded t) :
id                                      └───────┘        └─────┘         └───────┘        └─────┘ 
src                                      └───────┘        └─────┘           └───────┘        └─────┘
typ                                     └───────┘        └─────┘         └───────┘        └─────┘ 
doc                                      └───────┘        └─────┘           └───────┘        └─────┘
592    Hausdorff_dist s t ≤ diam (s ∪ t) :=
id     └────────────┘    └──┘    
src    └────────────┘      └──┘    
typ    └────────────┘    └──┘    
doc    └────────────┘       └──┘
593  begin
st   └─────
594    rcases hs with ⟨x, xs⟩,
id            └┘
src    └─────┘  └───────────┘
typ    └─────┘└┘└───────────┘
doc    └─────┘  └───────────┘
txt    └─────┘  └───────────┘
par    └─────┘  └───────────┘
pid            └───────────┘
st   ───────────────────────┘└─
595    rcases ht with ⟨y, yt⟩,
id            └┘
src    └─────┘  └───────────┘
typ    └─────┘└┘└───────────┘
doc    └─────┘  └───────────┘
txt    └─────┘  └───────────┘
par    └─────┘  └───────────┘
pid            └───────────┘
st   ───────────────────────┘└─
596    refine Hausdorff_dist_le_of_mem_dist diam_nonneg _ _,
id            └───────────────────────────┘ └─────────┘
src    └─────┘└───────────────────────────┘└─────────┘└──┘
typ    └─────┘└───────────────────────────┘└─────────┘└──┘
doc    └─────┘└───────────────────────────┘└─────────┘└──┘
txt    └─────┘                                        └──┘
par    └─────┘                                        └──┘
pid                                                  └──┘
st   ─────────────────────────────────────────────────────┘└─
597    { exact  λz hz, ⟨y, yt, dist_le_diam_of_mem (bounded_union.2 ⟨bs, bt⟩)
id                            └─────────────────┘  └───────────┘    └┘  └┘
src      └─────┘ └────┘  └┘  └┘└─────────────────┘ └───────────┘└─┘   └┘  └──
typ      └─────┘ └────┘ └┘  └┘└─────────────────┘ └───────────┘└─┘ └┘└┘└┘└──
doc      └─────┘ └────┘  └┘  └┘└─────────────────┘ └───────────┘└─┘   └┘  └──
txt      └─────┘ └────┘  └┘  └┘                                 └─┘   └┘  └──
par      └─────┘ └────┘  └┘  └┘                                 └─┘   └┘  └──
pid           └┘ └────┘  └┘  └┘                                 └─┘   └┘  └──
st   ───┘└────────────────────────────────────────────────────────────────────
598        (subset_union_left _ _ hz) (subset_union_right _ _ yt)⟩ },
id          └───────────────┘          └────────────────┘     └┘
src  ─────┘ └───────────────┘└───┘  └┘ └────────────────┘└───┘  └─┘
typ  ─────┘ └───────────────┘└───┘  └┘ └────────────────┘└───┘└┘└─┘
doc  ─────┘                  └───┘  └┘                   └───┘  └─┘
txt  ─────┘                  └───┘  └┘                   └───┘  └─┘
par  ─────┘                  └───┘  └┘                   └───┘  └─┘
pid  ─────┘                  └───┘  └┘                   └───┘  └┘
st   ─────────────────────────────────────────────────────────────┘└┘
599    { exact λz hz, ⟨x, xs, dist_le_diam_of_mem (bounded_union.2 ⟨bs, bt⟩)
id                           └─────────────────┘  └───────────┘    └┘  └┘
src      └────┘ └────┘  └┘  └┘└─────────────────┘ └───────────┘└─┘   └┘  └──
typ      └────┘ └────┘ └┘  └┘└─────────────────┘ └───────────┘└─┘ └┘└┘└┘└──
doc      └────┘ └────┘  └┘  └┘└─────────────────┘ └───────────┘└─┘   └┘  └──
txt      └────┘ └────┘  └┘  └┘                                 └─┘   └┘  └──
par      └────┘ └────┘  └┘  └┘                                 └─┘   └┘  └──
pid            └────┘  └┘  └┘                                 └─┘   └┘  └──
st   ────────────────────────────────────────────────────────────────────────
600        (subset_union_right _ _ hz) (subset_union_left _ _ xs)⟩ }
id          └────────────────┘          └───────────────┘     └┘
src  ─────┘ └────────────────┘└───┘  └┘ └───────────────┘└───┘  └─┘
typ  ─────┘ └────────────────┘└───┘  └┘ └───────────────┘└───┘└┘└─┘
doc  ─────┘                   └───┘  └┘                  └───┘  └─┘
txt  ─────┘                   └───┘  └┘                  └───┘  └─┘
par  ─────┘                   └───┘  └┘                  └───┘  └─┘
pid  ─────┘                   └───┘  └┘                  └───┘  └┘
st   ─────────────────────────────────────────────────────────────┘└─
601  end
st   ──┘
602  
603  /-- The distance to a set is controlled by the Hausdorff distance -/
604  lemma inf_dist_le_Hausdorff_dist_of_mem (hx : x ∈ s) (fin : Hausdorff_edist s t ≠ ⊤) :
id                                                            └─────────────┘    
src                                                             └─────────────┘      
typ                                                           └─────────────┘    
doc                                                              └─────────────┘
605    inf_dist x t ≤ Hausdorff_dist s t :=
id     └──────┘    └────────────┘  
src    └──────┘      └────────────┘
typ    └──────┘    └────────────┘  
doc    └──────┘       └────────────┘
606  begin
st   └─────
607    have ht : t.nonempty := nonempty_of_Hausdorff_edist_ne_top ⟨x, hx⟩ fin,
id               └────────┘    └────────────────────────────────┘    └┘  └─┘
src    └────────┘└────────┘└──┘└────────────────────────────────┘  └┘  └┘└─┘
typ    └────────┘└────────┘└──┘└────────────────────────────────┘ └┘└┘└┘└─┘
doc    └────────┘└────────┘└──┘└────────────────────────────────┘  └┘  └┘
txt    └────────┘          └──┘                                    └┘  └┘
par    └────────┘          └──┘                                    └┘  └┘
pid    └─────┘└─┘          └──┘                                    └┘  └┘
st   ───────────────────────────────────────────────────────────────────────┘└─
608    rw [Hausdorff_dist, inf_dist, ennreal.to_real_le_to_real (inf_edist_ne_top ht) fin],
id         └────────────┘  └──────┘  └────────────────────────┘  └──────────────┘ └┘  └─┘
src    └──┘└────────────┘└┘└──────┘└┘└────────────────────────┘ └──────────────┘  └┘└─┘
typ    └──┘└────────────┘└┘└──────┘└┘└────────────────────────┘ └──────────────┘└┘└┘└─┘
doc    └──┘└────────────┘└┘└──────┘└┘                           └──────────────┘  └┘   
txt    └──┘              └┘        └┘                                             └┘   
par    └──┘              └┘        └┘                                             └┘   
pid      └┘              └┘        └┘                                             └┘   
st   ───────────────────┘└────────┘└────────────────────────────────────────────────────┘└──
609    exact inf_edist_le_Hausdorff_edist_of_mem hx
id           └─────────────────────────────────┘ └┘
src    └────┘└─────────────────────────────────┘  
typ    └────┘└─────────────────────────────────┘└┘
doc    └────┘└─────────────────────────────────┘  
txt    └────┘                                     
par    └────┘                                     
pid                                              
st   ──────────────────────────────────────────────┘
610  end
st   └─┘
611  
612  /-- If the Hausdorff distance is `<r`, then any point in one of the sets is at distance
613  `<r` of a point in the other set -/
614  lemma exists_dist_lt_of_Hausdorff_dist_lt {r : ℝ} (h : x ∈ s) (H : Hausdorff_dist s t < r)
id                                                                  └────────────┘    
src                                                                   └────────────┘     
typ                                                                 └────────────┘    
doc                                                                     └────────────┘
615    (fin : Hausdorff_edist s t ≠ ⊤) : ∃y∈t, dist x y < r :=
id            └─────────────┘          └──┘    
src           └─────────────┘              └──┘     
typ           └─────────────┘          └──┘    
doc           └─────────────┘
616  begin
st   └─────
617    have r0 : 0 < r := lt_of_le_of_lt (Hausdorff_dist_nonneg) H,
id                      └────────────┘  └───────────────────┘  
src    └──────────┘ └──┘└────────────┘ └───────────────────┘└┘
typ    └──────────┘└──┘└────────────┘ └───────────────────┘└┘
doc    └──────────┘  └──┘               └───────────────────┘└┘
txt    └──────────┘  └──┘                                    └┘
par    └──────────┘  └──┘                                    └┘
pid    └─────┘└───┘  └──┘                                    └┘
st   ────────────────────────────────────────────────────────────┘└─
618    have : Hausdorff_edist s t < ennreal.of_real r,
id            └─────────────┘     └─────────────┘ 
src    └─────┘└─────────────┘   └─────────────┘
typ    └─────┘└─────────────┘ └─────────────┘
doc    └─────┘└─────────────┘   └─────────────┘
txt    └─────┘                                 
par    └─────┘                                 
pid    └───┘└┘                                 
st   ───────────────────────────────────────────────┘
619      by rwa [Hausdorff_dist, ← ennreal.to_real_of_real (le_of_lt r0),
id               └────────────┘    └─────────────────────┘  └──────┘ └┘
src         └───┘└────────────┘└──┘└─────────────────────┘ └──────┘  └──
typ         └───┘└────────────┘└──┘└─────────────────────┘ └──────┘└┘└──
doc         └───┘└────────────┘└──┘                                  └──
txt         └───┘              └──┘                                  └──
par         └───┘              └──┘                                  └──
pid            └┘              └──┘                                  └──
st               └────────────┘└───────────────────────────────────────┘└─
620              ennreal.to_real_lt_to_real fin (ennreal.of_real_ne_top)] at H,
id               └────────────────────────┘ └─┘  └────────────────────┘
src  ───────────┘└────────────────────────┘└─┘ └────────────────────┘└─────┘
typ  ───────────┘└────────────────────────┘└─┘ └────────────────────┘└─────┘
doc  ───────────┘                                                    └─────┘
txt  ───────────┘                                                    └─────┘
par  ───────────┘                                                    └─────┘
pid  ───────────┘                                                    └┘└───┘
st   ──────────────────────────────────────────────────────────────────┘     └─
621    rcases exists_edist_lt_of_Hausdorff_edist_lt h this with ⟨y, hy, yr⟩,
id            └───────────────────────────────────┘  └──┘
src    └─────┘└───────────────────────────────────┘     └───────────────┘
typ    └─────┘└───────────────────────────────────┘└──┘└───────────────┘
doc    └─────┘└───────────────────────────────────┘     └───────────────┘
txt    └─────┘                                          └───────────────┘
par    └─────┘                                          └───────────────┘
pid                                                    └───────────────┘
st   ─────────────────────────────────────────────────────────────────────┘└─
622    rw [edist_dist, ennreal.of_real_lt_of_real_iff r0] at yr,
id         └────────┘  └────────────────────────────┘ └┘
src    └──┘└────────┘└┘└────────────────────────────┘  └─────┘
typ    └──┘└────────┘└┘└────────────────────────────┘└┘└─────┘
doc    └──┘          └┘                                └─────┘
txt    └──┘          └┘                                └─────┘
par    └──┘          └┘                                └─────┘
pid      └┘          └┘                                └────┘
st   ───────────────┘└─────────────────────────────────┘└────┘└─
623    exact ⟨y, hy, yr⟩
id              └┘  └┘
src    └────┘  └┘  └┘  └┘
typ    └────┘ └┘└┘└┘└┘└┘
doc    └────┘  └┘  └┘  └┘
txt    └────┘  └┘  └┘  └┘
par    └────┘  └┘  └┘  └┘
pid           └┘  └┘  
st   ───────────────────┘
624  end
st   └─┘
625  
626  /-- If the Hausdorff distance is `<r`, then any point in one of the sets is at distance
627  `<r` of a point in the other set -/
628  lemma exists_dist_lt_of_Hausdorff_dist_lt' {r : ℝ} (h : y ∈ t) (H : Hausdorff_dist s t < r)
id                                                                   └────────────┘    
src                                                                    └────────────┘     
typ                                                                  └────────────┘    
doc                                                                      └────────────┘
629    (fin : Hausdorff_edist s t ≠ ⊤) : ∃x∈s, dist x y < r :=
id            └─────────────┘          └──┘    
src           └─────────────┘              └──┘     
typ           └─────────────┘          └──┘    
doc           └─────────────┘
630  begin
st   └─────
631    rw Hausdorff_dist_comm at H,
id        └─────────────────┘
src    └─┘└─────────────────┘└───┘
typ    └─┘└─────────────────┘└───┘
doc    └─┘└─────────────────┘└───┘
txt    └─┘                   └───┘
par    └─┘                   └───┘
pid                         └───┘
st   ────────────────────────────┘└─
632    rw Hausdorff_edist_comm at fin,
id        └──────────────────┘
src    └─┘└──────────────────┘└─────┘
typ    └─┘└──────────────────┘└─────┘
doc    └─┘└──────────────────┘└─────┘
txt    └─┘                    └─────┘
par    └─┘                    └─────┘
pid                          └─────┘
st   ───────────────────────────────┘└─
633    simpa [dist_comm] using exists_dist_lt_of_Hausdorff_dist_lt h H fin
id            └───────┘        └─────────────────────────────────┘   └─┘
src    └─────┘└───────┘└──────┘└─────────────────────────────────┘  └─┘
typ    └─────┘└───────┘└──────┘└─────────────────────────────────┘└─┘
doc    └─────┘         └──────┘└─────────────────────────────────┘     
txt    └─────┘         └──────┘                                        
par    └─────┘         └──────┘                                        
pid                  └────┘                                        
st   ─────────────────────────────────────────────────────────────────────┘
634  end
st   └─┘
635  
636  /-- The infimum distance to `s` and `t` are the same, up to the Hausdorff distance
637  between `s` and `t` -/
638  lemma inf_dist_le_inf_dist_add_Hausdorff_dist (fin : Hausdorff_edist s t ≠ ⊤) :
id                                                        └─────────────┘    
src                                                       └─────────────┘      
typ                                                       └─────────────┘    
doc                                                       └─────────────┘
639    inf_dist x t ≤ inf_dist x s + Hausdorff_dist s t :=
id     └──────┘    └──────┘    └────────────┘  
src    └──────┘      └──────┘      └────────────┘
typ    └──────┘    └──────┘    └────────────┘  
doc    └──────┘       └──────┘       └────────────┘
640  begin
st   └─────
641    rcases empty_or_nonempty_of_Hausdorff_edist_ne_top fin with ⟨hs,ht⟩|⟨hs,ht⟩,
id            └─────────────────────────────────────────┘ └─┘
src    └─────┘└─────────────────────────────────────────┘└─┘└───────────────────┘
typ    └─────┘└─────────────────────────────────────────┘└─┘└───────────────────┘
doc    └─────┘                                              └───────────────────┘
txt    └─────┘                                              └───────────────────┘
par    └─────┘                                              └───────────────────┘
pid                                                        └───────────────────┘
st   ────────────────────────────────────────────────────────────────────────────┘└─
642    { simp only [hs, ht, Hausdorff_dist_empty, inf_dist_empty, zero_add] },
id                  └┘  └┘  └──────────────────┘  └────────────┘  └──────┘
src      └─────────┘  └┘  └┘└──────────────────┘└┘└────────────┘└┘└──────┘└┘
typ      └─────────┘└┘└┘└┘└┘└──────────────────┘└┘└────────────┘└┘└──────┘└┘
doc      └─────────┘  └┘  └┘└──────────────────┘└┘└────────────┘└┘        └┘
txt      └─────────┘  └┘  └┘                    └┘              └┘        └┘
par      └─────────┘  └┘  └┘                    └┘              └┘        └┘
pid          └──┘└┘  └┘  └┘                    └┘              └┘        
st   ───┘└─────────────────────────────────────────────────────────────────┘└┘
643    rw [inf_dist, inf_dist, Hausdorff_dist, ← ennreal.to_real_add (inf_edist_ne_top hs) fin,
id         └──────┘  └──────┘  └────────────┘    └─────────────────┘  └──────────────┘ └┘  └─┘
src    └──┘└──────┘└┘└──────┘└┘└────────────┘└──┘└─────────────────┘ └──────────────┘  └┘└─┘└─
typ    └──┘└──────┘└┘└──────┘└┘└────────────┘└──┘└─────────────────┘ └──────────────┘└┘└┘└─┘└─
doc    └──┘└──────┘└┘└──────┘└┘└────────────┘└──┘                    └──────────────┘  └┘   └─
txt    └──┘        └┘        └┘              └──┘                                      └┘   └─
par    └──┘        └┘        └┘              └──┘                                      └┘   └─
pid      └┘        └┘        └┘              └──┘                                      └┘   └─
st   ─────────────┘└────────┘└──────────────┘└───────────────────────────────────────────────┘└─
644        ennreal.to_real_le_to_real (inf_edist_ne_top ht)],
id         └────────────────────────┘  └──────────────┘ └┘
src  ─────┘└────────────────────────┘ └──────────────┘  └┘
typ  ─────┘└────────────────────────┘ └──────────────┘└┘└┘
doc  ─────┘                           └──────────────┘  └┘
txt  ─────┘                                             └┘
par  ─────┘                                             └┘
pid  ─────┘                                             └┘
st   ─────────────────────────────────────────────────────┘└──
645    { exact inf_edist_le_inf_edist_add_Hausdorff_edist },
id             └────────────────────────────────────────┘
src      └────┘└────────────────────────────────────────┘
typ      └────┘└────────────────────────────────────────┘
doc      └────┘└────────────────────────────────────────┘
txt      └────┘                                          
par      └────┘                                          
pid                                                     
st   ───┘└───────────────────────────────────────────────┘└┘
646    { exact ennreal.add_ne_top.2 ⟨inf_edist_ne_top hs, fin⟩ }
id             └────────────────┘    └──────────────┘ └┘  └─┘
src      └────┘└────────────────┘└─┘ └──────────────┘  └┘└─┘└┘
typ      └────┘└────────────────┘└─┘ └──────────────┘└┘└┘└─┘└┘
doc      └────┘                  └─┘ └──────────────┘  └┘   └┘
txt      └────┘                  └─┘                   └┘   └┘
par      └────┘                  └─┘                   └┘   └┘
pid                             └─┘                   └┘   
st   ─────────────────────────────────────────────────────────┘└─
647  end
st   ──┘
648  
649  /-- The Hausdorff distance is invariant under isometries -/
650  lemma Hausdorff_dist_image (h : isometry Φ) :
id                                   └──────┘ 
src                                  └──────┘
typ                                  └──────┘ 
doc                                  └──────┘
651    Hausdorff_dist (Φ '' s) (Φ '' t) = Hausdorff_dist s t :=
id     └────────────┘   └┘     └┘    └────────────┘  
src    └────────────┘    └┘       └┘     └────────────┘
typ    └────────────┘   └┘     └┘    └────────────┘  
doc    └────────────┘                     └────────────┘
652  by simp [Hausdorff_dist, Hausdorff_edist_image h]
id            └────────────┘  └───────────────────┘ 
src     └────┘└────────────┘└┘└───────────────────┘ └─
typ     └────┘└────────────┘└┘└───────────────────┘└─
doc     └────┘└────────────┘└┘└───────────────────┘ └─
txt     └────┘              └┘                      └─
par     └────┘              └┘                      └─
pid                       └┘                      
st     └───────────────────────────────────────────────
653  
src  
typ  
doc  
txt  
par  
pid  
st   
654  /-- The Hausdorff distance satisfies the triangular inequality -/
655  lemma Hausdorff_dist_triangle (fin : Hausdorff_edist s t ≠ ⊤) :
id                                        └─────────────┘    
src                                       └─────────────┘      
typ                                       └─────────────┘    
doc                                       └─────────────┘
656    Hausdorff_dist s u ≤ Hausdorff_dist s t + Hausdorff_dist t u :=
id     └────────────┘    └────────────┘    └────────────┘  
src    └────────────┘      └────────────┘      └────────────┘
typ    └────────────┘    └────────────┘    └────────────┘  
doc    └────────────┘       └────────────┘       └────────────┘
657  begin
st   └─────
658    by_cases Hausdorff_edist s u = ⊤,
id              └─────────────┘    
src    └───────┘└─────────────┘  
typ    └───────┘└─────────────┘
doc    └───────┘└─────────────┘   
txt    └───────┘                  
par    └───────┘                  
pid                              
st   ─────────────────────────────────┘└─
659    { calc Hausdorff_dist s u = 0 + 0 : by simp [Hausdorff_dist, h]
id       └──┘                                      └────────────┘  
src      └──┘                                └────┘└────────────┘└┘ └─
typ      └──┘                                └────┘└────────────┘└┘└─
doc      └──┘                                 └────┘└────────────┘└┘ └─
txt                                           └────┘              └┘ └─
par                                           └────┘              └┘ └─
pid                                                             └┘ 
st   ───┘└──────────────────────────────────┘└─────────────────────────
660           ... ≤ Hausdorff_dist s t + Hausdorff_dist t u :
id                                      └────────────┘  
src  ────────┘                           └────────────┘
typ  ────────┘                          └────────────┘  
doc  ────────┘                           └────────────┘
txt  ────────┘
par  ────────┘
pid  ────────┘
st   ────────┘└───────────────────────────────────────────────
661             add_le_add (Hausdorff_dist_nonneg) (Hausdorff_dist_nonneg) },
id              └────────┘                          └───────────────────┘
src             └────────┘                          └───────────────────┘
typ             └────────┘                          └───────────────────┘
doc                                                 └───────────────────┘
st   ────────────────────────────────────────────────────────────────────┘└─┘
662    { have Dtu : Hausdorff_edist t u < ⊤ := calc
id                  └─────────────┘   
src      └─────────┘└─────────────┘   └──┘    
typ      └─────────┘└─────────────┘ └──┘    
doc      └─────────┘└─────────────┘    └──┘    
txt      └─────────┘                   └──┘    
par      └─────────┘                   └──┘    
pid      └──────┘└─┘                   └──┘    
st   ───────────────────────────────────────────────
663        Hausdorff_edist t u ≤ Hausdorff_edist t s + Hausdorff_edist s u : Hausdorff_edist_triangle
id                                                    └─────────────┘     └──────────────────────┘
src  ─────┘                                    └─────────────┘  └─┘└──────────────────────┘
typ  ─────┘                                   └─────────────┘└─┘└──────────────────────┘
doc  ─────┘                                    └─────────────┘  └─┘└──────────────────────┘
txt  ─────┘                                                     └─┘                        
par  ─────┘                                                     └─┘                        
pid  ─────┘                                                     └─┘                        
st   ─────────────────────────────────────────────────────────────────────────────────────────────────
664        ... = Hausdorff_edist s t + Hausdorff_edist s u : by simp [Hausdorff_edist_comm]
id                                                                    └──────────────────┘
src  ─────────┘                                    └─┘  └────┘└──────────────────┘└─
typ  ─────────┘                                    └─┘  └────┘└──────────────────┘└─
doc  ─────────┘                                    └─┘  └────┘└──────────────────┘└─
txt  ─────────┘                                    └─┘  └────┘                    └─
par  ─────────┘                                    └─┘  └────┘                    └─
pid  ─────────┘                                    └─┘  └─────┘                    └─
st   ─────────────────────────────────────────────────────────┘└────────────────────────────
665        ... < ⊤ : by simp  [ennreal.add_lt_top]; simp [ennreal.lt_top_iff_ne_top, h, fin],
id                             └────────────────┘         └───────────────────────┘    └─┘
src  ─────┘└──┘  └─┘  └─────┘└────────────────┘└┘└────┘└───────────────────────┘└┘ └┘└─┘
typ  ─────┘└──┘  └─┘  └─────┘└────────────────┘└┘└────┘└───────────────────────┘└┘└┘└─┘
doc  ─────┘└──┘  └─┘  └─────┘                  └┘└────┘                         └┘ └┘   
txt  ─────┘└──┘  └─┘  └─────┘                  └┘└────┘                         └┘ └┘   
par  ─────┘└──┘  └─┘  └─────┘                  └┘└────┘                         └┘ └┘   
pid  ─────────┘  └─┘  └──────┘                  └───────┘                         └┘ └┘   
st   ─────┘└──────────┘└───────────────────────────────────────────────────────────────────┘└─
666      rw [Hausdorff_dist, Hausdorff_dist, Hausdorff_dist,
id           └────────────┘  └────────────┘  └────────────┘
src      └──┘└────────────┘└┘└────────────┘└┘└────────────┘└─
typ      └──┘└────────────┘└┘└────────────┘└┘└────────────┘└─
doc      └──┘└────────────┘└┘└────────────┘└┘└────────────┘└─
txt      └──┘              └┘              └┘              └─
par      └──┘              └┘              └┘              └─
pid        └┘              └┘              └┘              └─
st   ─────────────────────┘└──────────────┘└──────────────┘└─
667          ← ennreal.to_real_add fin (lt_top_iff_ne_top.1 Dtu), ennreal.to_real_le_to_real h],
id             └─────────────────┘ └─┘  └───────────────┘   └─┘   └────────────────────────┘ 
src  ─────────┘└─────────────────┘└─┘ └───────────────┘└─┘   └─┘└────────────────────────┘ 
typ  ─────────┘└─────────────────┘└─┘ └───────────────┘└─┘└─┘└─┘└────────────────────────┘
doc  ─────────┘                                        └─┘   └─┘                           
txt  ─────────┘                                        └─┘   └─┘                           
par  ─────────┘                                        └─┘   └─┘                           
pid  ─────────┘                                        └─┘   └─┘                           
st   ──────────────────────────────────────────────────────────┘└────────────────────────────┘└──
668      { exact Hausdorff_edist_triangle },
id               └──────────────────────┘
src        └────┘└──────────────────────┘
typ        └────┘└──────────────────────┘
doc        └────┘└──────────────────────┘
txt        └────┘                        
par        └────┘                        
pid                                     
st   ─────┘└─────────────────────────────┘└┘
669      { simp [ennreal.add_eq_top, lt_top_iff_ne_top.1 Dtu, fin] }}
id               └────────────────┘  └───────────────┘   └─┘  └─┘
src        └────┘└────────────────┘└┘└───────────────┘└─┘   └┘└─┘└┘
typ        └────┘└────────────────┘└┘└───────────────┘└─┘└─┘└┘└─┘└┘
doc        └────┘                  └┘                 └─┘   └┘   └┘
txt        └────┘                  └┘                 └─┘   └┘   └┘
par        └────┘                  └┘                 └─┘   └┘   └┘
pid                              └┘                 └─┘   └┘   
st   ─────────────────────────────────────────────────────────────┘└──
670  end
st   ──┘
671  
672  /-- The Hausdorff distance satisfies the triangular inequality -/
673  lemma Hausdorff_dist_triangle' (fin : Hausdorff_edist t u ≠ ⊤) :
id                                         └─────────────┘    
src                                        └─────────────┘      
typ                                        └─────────────┘    
doc                                        └─────────────┘
674    Hausdorff_dist s u ≤ Hausdorff_dist s t + Hausdorff_dist t u :=
id     └────────────┘    └────────────┘    └────────────┘  
src    └────────────┘      └────────────┘      └────────────┘
typ    └────────────┘    └────────────┘    └────────────┘  
doc    └────────────┘       └────────────┘       └────────────┘
675  begin
st   └─────
676    rw Hausdorff_edist_comm at fin,
id        └──────────────────┘
src    └─┘└──────────────────┘└─────┘
typ    └─┘└──────────────────┘└─────┘
doc    └─┘└──────────────────┘└─────┘
txt    └─┘                    └─────┘
par    └─┘                    └─────┘
pid                          └─────┘
st   ───────────────────────────────┘└─
677    have I : Hausdorff_dist u s ≤ Hausdorff_dist u t + Hausdorff_dist t s := Hausdorff_dist_triangle fin,
id                                                     └────────────┘      └─────────────────────┘ └─┘
src    └───────┘                                └────────────┘  └──┘└─────────────────────┘└─┘
typ    └───────┘                               └────────────┘└──┘└─────────────────────┘└─┘
doc    └───────┘                                  └────────────┘  └──┘└─────────────────────┘
txt    └───────┘                                                  └──┘                       
par    └───────┘                                                  └──┘                       
pid    └────┘└─┘                                                  └──┘                       
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
678    simpa [add_comm, Hausdorff_dist_comm] using I
id            └──────┘  └─────────────────┘        
src    └─────┘└──────┘└┘└─────────────────┘└──────┘ 
typ    └─────┘└──────┘└┘└─────────────────┘└──────┘
doc    └─────┘        └┘└─────────────────┘└──────┘ 
txt    └─────┘        └┘                   └──────┘ 
par    └─────┘        └┘                   └──────┘ 
pid                 └┘                   └────┘ 
st   ───────────────────────────────────────────────┘
679  end
st   └─┘
680  
681  /-- The Hausdorff distance between a set and its closure vanish -/
682  @[simp] lemma Hausdorff_dist_self_closure : Hausdorff_dist s (closure s) = 0 :=
id                                               └────────────┘   └─────┘   
src                                              └────────────┘    └─────┘    
typ                                              └────────────┘   └─────┘   
doc    └──┘                                      └────────────┘    └─────┘
683  by simp [Hausdorff_dist]
id            └────────────┘
src     └────┘└────────────┘└─
typ     └────┘└────────────┘└─
doc     └────┘└────────────┘└─
txt     └────┘              └─
par     └────┘              └─
pid                       
st     └──────────────────────
684  
src  
typ  
doc  
txt  
par  
pid  
st   
685  /-- Replacing a set by its closure does not change the Hausdorff distance. -/
686  @[simp] lemma Hausdorff_dist_closure₁ : Hausdorff_dist (closure s) t = Hausdorff_dist s t :=
id                                           └────────────┘  └─────┘     └────────────┘  
src                                          └────────────┘  └─────┘       └────────────┘
typ                                          └────────────┘  └─────┘     └────────────┘  
doc    └──┘                                  └────────────┘  └─────┘        └────────────┘
687  by simp [Hausdorff_dist]
id            └────────────┘
src     └────┘└────────────┘└─
typ     └────┘└────────────┘└─
doc     └────┘└────────────┘└─
txt     └────┘              └─
par     └────┘              └─
pid                       
st     └──────────────────────
688  
src  
typ  
doc  
txt  
par  
pid  
st   
689  /-- Replacing a set by its closure does not change the Hausdorff distance. -/
690  @[simp] lemma Hausdorff_dist_closure₂ : Hausdorff_dist s (closure t) = Hausdorff_dist s t :=
id                                           └────────────┘   └─────┘    └────────────┘  
src                                          └────────────┘    └─────┘     └────────────┘
typ                                          └────────────┘   └─────┘    └────────────┘  
doc    └──┘                                  └────────────┘    └─────┘      └────────────┘
691  by simp [Hausdorff_dist]
id            └────────────┘
src     └────┘└────────────┘└─
typ     └────┘└────────────┘└─
doc     └────┘└────────────┘└─
txt     └────┘              └─
par     └────┘              └─
pid                       
st     └──────────────────────
692  
src  
typ  
doc  
txt  
par  
pid  
st   
693  /-- The Hausdorff distance between two sets and their closures coincide -/
694  @[simp] lemma Hausdorff_dist_closure : Hausdorff_dist (closure s) (closure t) = Hausdorff_dist s t :=
id                                          └────────────┘  └─────┘    └─────┘    └────────────┘  
src                                         └────────────┘  └─────┘     └─────┘     └────────────┘
typ                                         └────────────┘  └─────┘    └─────┘    └────────────┘  
doc    └──┘                                 └────────────┘  └─────┘     └─────┘      └────────────┘
695  by simp [Hausdorff_dist]
id            └────────────┘
src     └────┘└────────────┘└─
typ     └────┘└────────────┘└─
doc     └────┘└────────────┘└─
txt     └────┘              └─
par     └────┘              └─
pid                       
st     └──────────────────────
696  
src  
typ  
doc  
txt  
par  
pid  
st   
697  /-- Two sets are at zero Hausdorff distance if and only if they have the same closures -/
698  lemma Hausdorff_dist_zero_iff_closure_eq_closure (fin : Hausdorff_edist s t ≠ ⊤) :
id                                                           └─────────────┘    
src                                                          └─────────────┘      
typ                                                          └─────────────┘    
doc                                                          └─────────────┘
699    Hausdorff_dist s t = 0 ↔ closure s = closure t :=
id     └────────────┘       └─────┘   └─────┘ 
src    └────────────┘         └─────┘    └─────┘
typ    └────────────┘       └─────┘   └─────┘ 
doc    └────────────┘           └─────┘     └─────┘
700  by simp [Hausdorff_edist_zero_iff_closure_eq_closure.symm, Hausdorff_dist,
id                                                              └────────────┘
src     └────┘                                                └┘└────────────┘└─
typ     └────┘└──────────────────────────────────────────────┘└┘└────────────┘└─
doc     └────┘                                                └┘└────────────┘└─
txt     └────┘                                                └┘              └─
par     └────┘                                                └┘              └─
pid                                                         └┘              └─
st     └────────────────────────────────────────────────────────────────────────
701           ennreal.to_real_eq_zero_iff, fin]
id            └─────────────────────────┘  └─┘
src  ────────┘└─────────────────────────┘└┘└─┘└─
typ  ────────┘└─────────────────────────┘└┘└─┘└─
doc  ────────┘                           └┘   └─
txt  ────────┘                           └┘   └─
par  ────────┘                           └┘   └─
pid  ────────┘                           └┘   
st   ───────────────────────────────────────────
702  
src  
typ  
doc  
txt  
par  
pid  
st   
703  /-- Two closed sets are at zero Hausdorff distance if and only if they coincide -/
704  lemma Hausdorff_dist_zero_iff_eq_of_closed (hs : is_closed s) (ht : is_closed t)
id                                                    └───────┘         └───────┘ 
src                                                   └───────┘          └───────┘
typ                                                   └───────┘         └───────┘ 
doc                                                   └───────┘          └───────┘
705    (fin : Hausdorff_edist s t ≠ ⊤) : Hausdorff_dist s t = 0 ↔ s = t :=
id            └─────────────┘        └────────────┘         
src           └─────────────┘          └────────────┘           
typ           └─────────────┘        └────────────┘         
doc           └─────────────┘            └────────────┘
706  by simp [(Hausdorff_edist_zero_iff_eq_of_closed hs ht).symm, Hausdorff_dist,
id             └───────────────────────────────────┘ └┘ └┘        └────────────┘
src     └────┘ └───────────────────────────────────┘    └──────┘└────────────┘└─
typ     └────┘ └───────────────────────────────────┘└┘└┘└──────┘└────────────┘└─
doc     └────┘ └───────────────────────────────────┘    └──────┘└────────────┘└─
txt     └────┘                                          └──────┘              └─
par     └────┘                                          └──────┘              └─
pid                                                   └──────┘              └─
st     └──────────────────────────────────────────────────────────────────────────
707           ennreal.to_real_eq_zero_iff, fin]
id            └─────────────────────────┘  └─┘
src  ────────┘└─────────────────────────┘└┘└─┘└─
typ  ────────┘└─────────────────────────┘└┘└─┘└─
doc  ────────┘                           └┘   └─
txt  ────────┘                           └┘   └─
par  ────────┘                           └┘   └─
pid  ────────┘                           └┘   
st   ───────────────────────────────────────────
708  
src  
typ  
doc  
txt  
par  
pid  
st   
709  end --section
710  end metric --namespace